diff options
| author | David Aspinall | 1999-08-23 19:59:14 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-08-23 19:59:14 +0000 |
| commit | dd87a4529bb3cee63301d2c6a017fd082349c16a (patch) | |
| tree | 5bdeae4af13b6965a095d842fafb8b1919a665af /CHANGES | |
| parent | da7e95bfddfcf9d33a2aa80026456b6f0cabf8c6 (diff) | |
Changes for 2.3 series pre-releases.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 53 |
1 files changed, 20 insertions, 33 deletions
@@ -1,43 +1,30 @@ -Summary of Changes for Proof General 2.1 ----------------------------------------- +Summary of Changes for Proof General 2.2 from 2.1 +------------------------------------------------- -* Supports Coq 6.3. +No changes yet. -* Supports Isabelle 99. Will not work with Isabelle 98. -* Two new provisional instantiations of Proof General, for: - ** Isabelle/Isar (new proof language for Isabelle) by - Markus Wenzel <wenzelm@informatik.tu-muenchen.de> - ** Plastic (http://www.dur.ac.uk/CARG/plastic.html) - by Paul Callaghan <P.C.Callaghan@durham.ac.uk>. -* Documentation improvements. - Information added for Coq mode. -* In proof-site.el, the environment variable PROOFGENERAL_ASSISTANTS - is examined for the default value of proof-assistants. No - editing of proof-site.el should be needed now. +Plan of Major Changes for Proof General 2.2 +------------------------------------------- -* Support for x-symbol package to beautify input and output with - special fonts. - Patches for Isabelle provided by David von Oheimb. - (work in progress) -* Improvements to Isabelle mode: multiple file handling now - more robust and handled by Isabelle primitives. - Support added by Markus Wenzel. +* 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) + +Please send details of any other improvements or bug fixes you would +like to see, to proofgen@dcs.ed.ac.uk. + -* Improvements to Coq mode: better recognition of - Coq syntax, support for proof-shell-restart-cmd. -* Toolbar can now be switched on and off via menu. - Several other usability improvements added to menus. -* Bug fixes: - - Long-lines with funny characters causing ^G's in Solaris. - - Templates in Isabelle theory file mode. - - Fix for case-insensitive matching. Added proof-case-fold-search - configuration variable to allow for proof script languages with - case-insensitive syntax. - - Process killing made robust. - - Regular expression fixes causing "nil extent" errors. |
