From dd87a4529bb3cee63301d2c6a017fd082349c16a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 23 Aug 1999 19:59:14 +0000 Subject: Changes for 2.3 series pre-releases. --- CHANGES | 53 ++++++++++++++++++++--------------------------------- 1 file changed, 20 insertions(+), 33 deletions(-) (limited to 'CHANGES') 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 - ** Plastic (http://www.dur.ac.uk/CARG/plastic.html) - by Paul Callaghan . -* 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. -- cgit v1.2.3