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 +++++++++++++++++++-------------------------------- Makefile.devel | 4 ++-- doc/ProofGeneral.texi | 4 ++-- html/download.phtml | 24 +++++++++++------------ 4 files changed, 36 insertions(+), 49 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 - ** 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. diff --git a/Makefile.devel b/Makefile.devel index 762cd7bb..dbd439bb 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -51,7 +51,7 @@ # Release tag. For pre-releases. Watch out with # substitution in tag target below, which edits $(DOWNLOADHTML) -PRERELEASE_TAG=2.1pre$(shell date "+%y%m%d") +PRERELEASE_TAG=2.2pre$(shell date "+%y%m%d") PREREL_TAG_FILE=prereltag.txt # html/download.phtml @@ -243,7 +243,7 @@ tag: # Edit $(DOWNLOADHTML) only for prereleases. # Careful: the sed command below relies on previous value of PRERELEASE_TAG. if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \ - (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ + (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.2pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \ fi # This hack to SOURCE: name is only needed because we have an obsolete version # of rpm installed on standard machines at dcs.ed, and we have to build with diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 1a875769..765d3eff 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -50,7 +50,7 @@ @set version 2.1 -@set xemacsversion 20.4 +@set xemacsversion 21.1 @set fsfversion 20.2 @set last-update August 1999 @set rcsid $Id$ @@ -1376,7 +1376,7 @@ The packages currently supported are @code{font-lock} @code{fume-func}, @vindex isa-mode-hooks @cindex font-lock @cindex colour -In XEmacs 20.4, proof script buffer are coloured (fontified as they say) +In XEmacs, proof script buffer are coloured (fontified as they say) by default. To automatically switch on fontification in FSF GNU Emacs 20.2, you need to configure the @code{font-lock} package yourself. This can be achieved by modifying the @var{prover}-mode-hooks where @var{prover} is either diff --git a/html/download.phtml b/html/download.phtml index ec5f20e7..939b691b 100644 --- a/html/download.phtml +++ b/html/download.phtml @@ -20,7 +20,7 @@ You can download the latest stable release, ProofGeneral-2.1, or the latest pre-release, -ProofGeneral-2.1pre990823. +ProofGeneral-2.2pre990823. There is also a complete archive of the current pre-release for developers. @@ -33,8 +33,7 @@ you may wish to check the

- Proof General Version 2.1, coming very soon! - + Proof General Version 2.1, released 23 August 1999

@@ -45,7 +44,7 @@ It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle version 99.

Check the file -for a summary of changes since the last stable version. +for a summary of changes since version 2.0.
Proof General is available in two formats:

@@ -103,7 +102,7 @@ any problems, suggestions, or patches.
-

Pre-release: ProofGeneral-2.1pre990823

+

Pre-release: ProofGeneral-2.2pre990823

@@ -112,9 +111,10 @@ features are added and experimented with.
Check the - file + file -for a summary of changes since the last stable version. +for a summary of changes since the last stable version, and +the planned changes to come.
Please test with the current pre-release before reporting any problems in a pre-release. @@ -123,13 +123,13 @@ in a pre-release.

@@ -153,7 +153,7 @@ have the right tools! @@ -163,7 +163,7 @@ You probably don't need to download this if you're only interested in hacking the Emacs lisp part of the program (but you may still like to check the latest -). +).

-- cgit v1.2.3