Changes for 2.3 series pre-releases.

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 <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>