diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 11:51:54 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 11:51:54 +0000 |
commit | b443769547c427f14b6f0618be569468510051c1 (patch) | |
tree | 5f39d1ff689cbbfa96ce051daffaf44ac08ade4d /TODO | |
parent | 2add3f415474f31c6b82981573a0cd3969fe7aab (diff) |
Updated for version 2.0
Diffstat (limited to 'TODO')
-rw-r--r-- | TODO | 33 |
1 files changed, 17 insertions, 16 deletions
@@ -6,35 +6,36 @@ proofgen@dcs.ed.ac.uk. Thanks! SHORT TERM ---------- * Fix bugs and improve code and documentation + Based on user feedback. MEDIUM TERM ----------- -* Provide a sensible default frame/buffer layout - * Add an example instantiation of Proof General - with no prover-specific extensions (probably for Isabelle) + using no prover-specific extensions (perhaps for Isabelle) -* Improve process handling 1: disable interrupts and/or catch - errors at crucial points in code so that C-g can safely be - used during script processing. +* Improve process handling 1 + Disable interrupts and/or catch errors at crucial points + in code so that C-g can safely be used during script + processing. Handle deleted buffers smoothly. LONGER TERM ----------- -* Add a browser mode for browsing script files and/or - theory data-structures in the prover. +* Add a browser mode for browsing script files + and/or theory data-structures in the prover. * Add more per-prover functions: menus for tactics, etc. -* Improve process handling 2: because Emacs is single-threaded, - no process output can be dealt with when we are running some - command. This means that it would be safe to extend the - red region, by putting more commands on the queue. Also it would - be safe to implement a clever undo command which worked on the +* Improve process handling 2 + Because Emacs is single-threaded, no process output can be + dealt with when we are running some command. + This means that it would be safe to extend the red region, + by putting more commands on the queue. Also it would be safe to + implement a clever undo command which worked on the red region: if there are commands waiting to be processed, we - could remove them from the queue. If there are no commands waiting, - we have to wait until something becomes blue to undo it by sending - a command to the process. + could remove them from the queue. If there are no commands + waiting, we have to wait until something becomes blue to + undo it by sending a command to the process. |