diff options
| -rw-r--r-- | CHANGES | 53 | ||||
| -rw-r--r-- | Makefile.devel | 4 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 4 | ||||
| -rw-r--r-- | html/download.phtml | 24 |
4 files changed, 36 insertions, 49 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. 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, <a href="#stable">ProofGeneral-2.1</a>, or the latest pre-release, <!-- Warning, next line edited by make file --> -<a href="#prerel">ProofGeneral-2.1pre990823</a>. +<a href="#prerel">ProofGeneral-2.2pre990823</a>. There is also a complete archive of the current pre-release <a href="#devel">for developers</a>. @@ -33,8 +33,7 @@ you may wish to check the <hr> <h2><a name="stable"> - Proof General Version 2.1, coming very soon! - <!-- released 23 August 1999 --> + Proof General Version 2.1, released 23 August 1999 </a> </h2> @@ -45,7 +44,7 @@ It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle version 99. <p> Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file -for a summary of changes since the last stable version. +for a summary of changes since version 2.0. <br> Proof General is available in two formats: </p> @@ -103,7 +102,7 @@ any problems, suggestions, or patches. <hr> <!-- WARNING! Line below automatically edited by makefile. --> -<h2><a name="prerel">Pre-release: ProofGeneral-2.1pre990823</a></h2> +<h2><a name="prerel">Pre-release: ProofGeneral-2.2pre990823</a></h2> <!-- End Warning. --> <p> @@ -112,9 +111,10 @@ features are added and experimented with. <br> Check the <!-- WARNING! Line below automatically edited by makefile. --> -<?php fileshow("ProofGeneral-2.1pre990823/CHANGES","CHANGES"); ?> file +<?php fileshow("ProofGeneral-2.2pre990823/CHANGES","CHANGES"); ?> file <!-- End Warning. --> -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. <br> Please test with the current pre-release before reporting any problems in a pre-release. @@ -123,13 +123,13 @@ in a pre-release. <ul> <!-- WARNING! Lines below automatically edited by makefile. --> <li> gzip'ed tar file: - <?php download_link("ProofGeneral-2.1pre990823.tar.gz") ?> + <?php download_link("ProofGeneral-2.2pre990823.tar.gz") ?> </li> <li> Linux RPM package - <?php download_link("ProofGeneral-2.1pre990823-1.noarch.rpm") ?> + <?php download_link("ProofGeneral-2.2pre990823-1.noarch.rpm") ?> <br> The source RPM is - <?php download_link("ProofGeneral-2.1pre990823-1.src.rpm","here") ?>. + <?php download_link("ProofGeneral-2.2pre990823-1.src.rpm","here") ?>. </li> <!-- End Warning. --> </ul> @@ -153,7 +153,7 @@ have the right tools! <ul> <li> gzip'ed tar file: <!-- WARNING! Line below automatically edited by makefile. --> - <?php download_link("ProofGeneral-2.1pre990823-devel.tar.gz") ?> + <?php download_link("ProofGeneral-2.2pre990823-devel.tar.gz") ?> <!-- End Warning. --> </li> </ul> @@ -163,7 +163,7 @@ You probably <em>don't</em> 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 <!-- WARNING! Line below automatically edited by makefile. --> -<?php fileshow("ProofGeneral-2.1pre990823/todo","low-level to-do list"); ?>). +<?php fileshow("ProofGeneral-2.2pre990823/todo","low-level to-do list"); ?>). <!-- End Warning. --> </p> |