From 3ea697a32ab2539c16ad797dfc350753688ad4dc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 23 Sep 2000 16:57:32 +0000 Subject: Updated --- TODO | 46 ++++++++-------------------------------------- 1 file changed, 8 insertions(+), 38 deletions(-) diff --git a/TODO b/TODO index 3dab3a4e..354bc695 100644 --- a/TODO +++ b/TODO @@ -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 . - [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 -- cgit v1.2.3