aboutsummaryrefslogtreecommitdiffhomepage
path: root/TODO
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-06-27 15:27:44 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-06-27 15:27:44 +0000
commit61e83559cb7614a71834f3c513c6638d54e89904 (patch)
treea48d4d2d2cab8bb1f8f4e594547802810ac714ee /TODO
parent840f589d751c08906ab6275c73c241167bb66214 (diff)
Updated
Diffstat (limited to 'TODO')
-rw-r--r--TODO18
1 files changed, 11 insertions, 7 deletions
diff --git a/TODO b/TODO
index 4fc5eb3e..4051676f 100644
--- a/TODO
+++ b/TODO
@@ -17,22 +17,26 @@ Plans for upcoming 3.x versions
* Support turning on/off prover output automatically, e.g.
Coq's "Begin Silent" and "End Silent" commands.
+ [Now implemented in 3.2pre]
* Fix Isabelle's "Stack overflow in regexp". See isa/BUGS.
-
-* Make an XEmacs package
-
-* Support more proof assistants
+ [Now implemented in 3.2pre]
* New key bindings for prover specific commands.
This will unfortunately result in changing some bindings, but make
room for more and avoid the user-reserved sequences C-c <letter>.
-
-* A more flexible way of choosing which instance of PG we want,
- allowing matches on the buffer before choosing the mode function.
+ [Now implemented in 3.2pre]
* Add a favourites mechanism for proof commands issued using
point-and-click in goals buffer. Useful when pbp isn't supported.
+ [Now partially implemented in 3.2pre]
+
+* Make an XEmacs package
+
+* Support more proof assistants
+
+* A more flexible way of choosing which instance of PG we want,
+ allowing matches on the buffer before choosing the mode function.
* Isabelle PG: Non-blocking for .thy loading from .ML files.