Opened 17 years ago
Last modified 11 years ago
#96 new enhancement
Start/stop quiet: disable these and use statedisplay instead
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | 4:prover-isabelle | Keywords: | |
| Cc: |
Description
Small change in proof_general_pgip.ML: disable printing by default, and get the
broker or Emacs to eagerly query the state.
After this is changed in Isabelle, we must change the broker and interfaces.
Change History (4)
comment:1 Changed 17 years ago by
comment:2 Changed 17 years ago by
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.1.0 |
|---|
comment:3 Changed 17 years ago by
NB start/stop quiet commands are now achieved by =<setproverflag>= but meaning is unchanged currently.
Note: See
TracTickets for help on using
tickets.
This was proposed by Makarius in Munich. But actually it is less easy than it first seems, because of the queue of commands used by the broker/interface. If we wanted to step through several proof states (or other queries) in succession and retain their output, we would have to interleave extra queries within the existing queue of commands. Also, we might want to update the display when the user reveals the window, but in the meantime the prover has been sent a long-running command so is now busy.
This is a bit nasty. A better solution might be to indicate with a flag in the command request whether or not output should be given. This is cleaner than the stopquiet/stopquiet commands which assume a single logical stream of commands.