aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorDavid Aspinall1999-08-23 19:59:14 +0000
committerDavid Aspinall1999-08-23 19:59:14 +0000
commitdd87a4529bb3cee63301d2c6a017fd082349c16a (patch)
tree5bdeae4af13b6965a095d842fafb8b1919a665af /CHANGES
parentda7e95bfddfcf9d33a2aa80026456b6f0cabf8c6 (diff)
Changes for 2.3 series pre-releases.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES53
1 files changed, 20 insertions, 33 deletions
diff --git a/CHANGES b/CHANGES
index d3a5f1d3..572ec43b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.