aboutsummaryrefslogtreecommitdiffhomepage
path: root/TODO
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-08-24 18:13:58 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-08-24 18:13:58 +0000
commitd79684fa05d5970036aa92249aa1905a5c6ead12 (patch)
tree15863148ad0547d37e6bb7528d85bff7cece9f25 /TODO
parent25dbbfc1d752232d5194513f76b8f98fc4546dca (diff)
Updated
Diffstat (limited to 'TODO')
-rw-r--r--TODO28
1 files changed, 22 insertions, 6 deletions
diff --git a/TODO b/TODO
index 21bc59c9..3efba2d0 100644
--- a/TODO
+++ b/TODO
@@ -3,15 +3,23 @@ This is our brief list of planned things to do to Proof General.
Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk. Thanks!
-SHORT TERM
-----------
+Plan of Changes for Proof General 2.2
+--------------------------------------
+
* Fix bugs and improve code and documentation
Based on user feedback.
-MEDIUM TERM
------------
-* Add an example instantiation of Proof General
- using no prover-specific extensions (perhaps for Isabelle)
+* Queue manipulation improvment: allow to extend or reduce
+ during processing, with fewer "Proof Process Busy"
+ messages.
+
+* Font-lock based on annotations in proof assistant output.
+ Particularly: colouration for Isabelle variable names.
+
+* x-symbol support integration.
+
+* Isabelle PG: Non-blocking for .thy loading from .ML files.
+ (hopefully as happy side effect of queue improvement)
* Improve process handling 1
Disable interrupts and/or catch errors at crucial points
@@ -19,8 +27,16 @@ MEDIUM TERM
processing. Handle deleted buffers smoothly.
+MEDIUM TERM
+-----------
+
+* Add an example instantiation of Proof General
+ using no prover-specific extensions (perhaps for Isabelle)
+
+
LONGER TERM
-----------
+
* Add a browser mode for browsing script files
and/or theory data-structures in the prover.