diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-09-23 16:57:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-23 16:57:32 +0000 |
| commit | 3ea697a32ab2539c16ad797dfc350753688ad4dc (patch) | |
| tree | eb9f2430d5b8f9521afc2b09ccfc486eea7237eb /TODO | |
| parent | b897b3d16393819ccd34e64fa536e66b92cc949d (diff) | |
Updated
Diffstat (limited to 'TODO')
| -rw-r--r-- | TODO | 46 |
1 files changed, 8 insertions, 38 deletions
@@ -11,40 +11,23 @@ Please send any suggestions, comments, or offers of help to proofgen@dcs.ed.ac.uk. Thanks! +Plans for upcoming versions +--------------------------- -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. - [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>. - [Now implemented in 3.2pre] +* Support more proof assistants -* 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] +* Add a browser mode for browsing script files + and/or theory data-structures in the prover. -* Support more proof assistants +* More flexible goals buffer mode to allow menus of + common proof commands. * 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. - - -Plans for later versions ------------------------- - -* Make an XEmacs package - * Queue manipulation improvment: allow to extend or reduce during processing, with fewer "Proof Process Busy" messages. @@ -57,21 +40,8 @@ Plans for later versions of proof assistants. Alternative is to base markup of undoable regions on proof assistant output or messages. -* Add completion of theorem names, choice of proof commands, etc. - -* Add a browser mode for browsing script files - and/or theory data-structures in the prover. - -* More flexible goals buffer mode to allow menus of - common proof commands. - * Implement ideas in the Proof General White Paper. (See the Development section of the web page for a link). - - - - - - +* Make an XEmacs package |