diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:04:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:04:13 +0000 |
| commit | f2d1f72dc8bb8239f2deb41d5d022a99c4dbbb42 (patch) | |
| tree | 8698c758b6f52921f2a60e5bece5502af87e049b /TODO | |
| parent | a1f38c7d643246761804359354c11c6c183a9d20 (diff) | |
Updated
Diffstat (limited to 'TODO')
| -rw-r--r-- | TODO | 42 |
1 files changed, 27 insertions, 15 deletions
@@ -1,34 +1,43 @@ This is our brief list of planned things to do to Proof General. -See also the appenix "Plans and Ideas" in the manual, and -for low-level detail, the file "todo" in the developer release. +$Id$ + +See also the Proof General projects page on the web, under the +development section of the home page. Also, see the appendix "Plans +and Ideas" in the manual, and for low-level detail, the file "todo" in +the developer release. Please send any suggestions, comments, or offers of help to proofgen@dcs.ed.ac.uk. Thanks! -Plans for later 3.x versions ----------------------------- +Plans for upcoming 3.x versions +------------------------------- -* Addition of favourites mechanism for proof commands issued using - point-and-click in goals buffer. Useful when pbp isn't supported. +* Make an XEmacs package -* Queue manipulation improvment: allow to extend or reduce - during processing, with fewer "Proof Process Busy" - messages. +* 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. + +* Add a favourites mechanism for proof commands issued using + point-and-click in goals buffer. Useful when pbp isn't supported. * Isabelle PG: Non-blocking for .thy loading from .ML files. -* Improve process handling: disable interrupts and/or catch errors at - crucial points in code so that C-g can safely be used during script - processing. Handle deleted buffers smoothly. -* Make an XEmacs package +Plans for later versions +------------------------ + +* Queue manipulation improvment: allow to extend or reduce + during processing, with fewer "Proof Process Busy" messages. -Plans for even later versions ------------------------------ +* Improve process handling: disable interrupts and/or catch errors at + crucial points in code so that C-g can safely be used during script + processing. Handle deleted buffers smoothly. * Implement "Atomic Command Sequence" idea, or something like it. To allow more flexible understanding of undo behaviour @@ -43,6 +52,9 @@ Plans for even later versions * 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). + |