diff options
-rw-r--r-- | AUTHORS | 23 | ||||
-rw-r--r-- | BUGS | 7 | ||||
-rw-r--r-- | COPYING | 9 | ||||
-rw-r--r-- | TODO | 28 |
4 files changed, 42 insertions, 25 deletions
@@ -1,18 +1,19 @@ Current Authors/Maintainers: - David Aspinall <da@dcs.ed.ac.uk> - doc, etc, generic, html, images, isa - Patrick Loiseleur <Patrick.Loiseleur@lri.fr> - coq - Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - isar - Paul Callaghan <P.C.Callaghan@durham.ac.uk> - plastic, lego + David Aspinall <da@dcs.ed.ac.uk> + doc, etc, generic, html, images, isa + Markus Wenzel <wenzelm@informatik.tu-muenchen.de> + isar + Paul Callaghan <P.C.Callaghan@durham.ac.uk> + plastic, lego +>> Position vacant for Coq maintainer, offers welcome! + Previous Authors: - Thomas Kleymann (lego, doc, generic) - Healfdene Goguen (coq, generic, doc) - Dilip Sequeira (lego) + Thomas Kleymann (lego, doc, generic) + Healfdene Goguen (coq, generic, doc) + Dilip Sequeira (lego) + Patrick Loiseleur (coq) @@ -12,9 +12,10 @@ Generic problems ================ * Highlighting of locked (blue) and queue (red) regions in FSF Emacs -may be unreliable in some cases. Cause unknown. If you observe -this, please submit a bug report with details of your system. -Workaround: switch to using XEmacs. +may be unreliable (disappear) in some cases. Cause unknown. If you +observe this, please submit a bug report with details of your system +and any other information you think may be relevant. Workaround: +switch to using XEmacs. * Ordinary undo in script buffer can edit the "uneditable region" in XEmacs. This doesn't happen in FSFmacs. Test case: @@ -12,15 +12,14 @@ Edinburgh. purposes. 3. You accept Proof General "as is". The University of Edinburgh -makes no warranty in respect of Proof General. Nevertheless you are -encouraged to report to LFCS any problems with or suggestions for -improvement of Proof General. +provides no warranty of any kind in respect of Proof General. +Nevertheless you are encouraged to report to LFCS any problems with or +suggestions for improvement of Proof General. 5. You may freely modify Proof General on condition that any significant changes are notified to LFCS and made available to LFCS such that they may be incorporated within future releases of -Proof General and licenced under the conditions of this licence -agreement. +Proof General under these copying conditions. 6. You will acknowledge LFCS and The University of Edinburgh as the designers and implementors of Proof General in any relevant document @@ -3,15 +3,23 @@ This is our brief list of planned things to do to Proof General. Please send any suggestions, comments, or offers of help to proofgen@dcs.ed.ac.uk. Thanks! -SHORT TERM ----------- +Plan of Changes for Proof General 2.2 +-------------------------------------- + * Fix bugs and improve code and documentation Based on user feedback. -MEDIUM TERM ------------ -* Add an example instantiation of Proof General - using no prover-specific extensions (perhaps for Isabelle) +* Queue manipulation improvment: allow to extend or reduce + during processing, with fewer "Proof Process Busy" + messages. + +* Font-lock based on annotations in proof assistant output. + Particularly: colouration for Isabelle variable names. + +* x-symbol support integration. + +* Isabelle PG: Non-blocking for .thy loading from .ML files. + (hopefully as happy side effect of queue improvement) * Improve process handling 1 Disable interrupts and/or catch errors at crucial points @@ -19,8 +27,16 @@ MEDIUM TERM processing. Handle deleted buffers smoothly. +MEDIUM TERM +----------- + +* Add an example instantiation of Proof General + using no prover-specific extensions (perhaps for Isabelle) + + LONGER TERM ----------- + * Add a browser mode for browsing script files and/or theory data-structures in the prover. |