diff options
author | 2000-06-27 15:27:44 +0000 | |
---|---|---|
committer | 2000-06-27 15:27:44 +0000 | |
commit | 61e83559cb7614a71834f3c513c6638d54e89904 (patch) | |
tree | a48d4d2d2cab8bb1f8f4e594547802810ac714ee | |
parent | 840f589d751c08906ab6275c73c241167bb66214 (diff) |
Updated
-rw-r--r-- | TODO | 18 | ||||
-rw-r--r-- | todo | 5 |
2 files changed, 11 insertions, 12 deletions
@@ -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. @@ -29,11 +29,6 @@ X (Low) e.g. probably not worth spending time on *** Outstanding bugs to investigate -A Re-visiting files (in Isar, at least) doesn't lock them properly. - M-x isar-mode does. Why? - Also, when files are removed by typing in shell buffer, they - don't get uncoloured??? - C Undoing comments with FSF Emacs weirdness. Noticed with Emacs 20.6.1. Seems to affect all provers. Workaround: use C-c C-RET or C-c C-r instead. |