diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-30 11:46:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-30 11:46:31 +0000 |
| commit | 5b9297125c126a8598e753966594ad64b59c6aff (patch) | |
| tree | 0c65185881b149041c71e103f56a1d516ac448fc /TODO | |
| parent | f9c93a0c0f11e628cce126c39d7c0d9040e93733 (diff) | |
Updated
Diffstat (limited to 'TODO')
| -rw-r--r-- | TODO | 11 |
1 files changed, 7 insertions, 4 deletions
@@ -1,6 +1,7 @@ This is our brief list of planned things to do to Proof General. -See also the appenix "Plans and Ideas" in the manual. +See also the appenix "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! @@ -10,6 +11,9 @@ proofgen@dcs.ed.ac.uk. Thanks! Plans for later 3.x versions ---------------------------- +* Addition of favourites mechanism for proof commands issued using + point-and-click in goals buffer. Useful when pbp isn't supported. + * Queue manipulation improvment: allow to extend or reduce during processing, with fewer "Proof Process Busy" messages. @@ -22,15 +26,14 @@ Plans for later 3.x versions * Make an XEmacs package -* Fix known problems with 3.0 (see developers `todo') - Plans for even later versions ----------------------------- * Implement "Atomic Command Sequence" idea, or something like it. To allow more flexible understanding of undo behaviour - of proof assistants. + 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. |