Admin changes for version 2.2.

4 files changed, 45 insertions, 30 deletions

diff --git a/CHANGES b/CHANGES
index a3772345..502d47c0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,5 @@
 Summary of Changes for Proof General 2.2 from 2.1
--------------------------------------------------
+=================================================
 
 Generic Changes
 ---------------
@@ -23,9 +23,14 @@ Generic Changes
 
 * Menus and keybindings have been reorganized.  
   Now keybindings invoke the same functions as the toolbar.
+  In particular, C-c C-n and C-c C-u are simplified so that
+  they always process or retract exactly one command, rather
+  than one command beyond point.  Moreover, C-c C-u does not 
+  take an optional argument to delete the retracted text
+  (it was too easy for the user to accidently type C-u C-c C-u !)
 
 * Command C-c C-t (proof-try-command) removed in favour of C-c C-v
-  (proof-execute-minibuffer-cmd), which now possibly uses the
+  (proof-execute-minibuffer-cmd), which now uses the
   filter proof-state-preserving-p to check that a command is safe.
 
 * Terminal string now automatically added to command for C-c C-v 
@@ -67,6 +72,11 @@ Only in the developers' release
 Internal changes for developers to note
 ---------------------------------------
 
+* Many robustness improvements so that Proof General fails
+  gracefully when certain configuration settings are unset.
+  The aim is to make it easier to adapt to new proof
+  assistants.
+
 * proof-shell-leave-annotations-in-output variable has been added.
   This allows quick and dirty mark up of output from the proof
   assistant using special characters with codes above 128 and
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index d140173f..e889a383 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -49,10 +49,10 @@
 @c
 
 
-@set version 2.1
+@set version 2.2
 @set xemacsversion 21.1
 @set fsfversion 20.2
-@set last-update August 1999
+@set last-update October 1999
 @set rcsid $Id$
 
 @ifinfo
diff --git a/etc/announce b/etc/announce
index 893a8fc2..67b2997a 100644
--- a/etc/announce
+++ b/etc/announce
@@ -27,9 +27,9 @@ To: coq-club@pauillac.inria.fr,
       
 
         
-Subject: Proof General --- Version 2.1 release
+Subject: Proof General --- Version 2.2 release
 
-           Announcing  Proof General  Version 2.1
+           Announcing  Proof General  Version 2.2
 
    A Generic Emacs interface for Interactive Proof Assistants
 
@@ -46,7 +46,8 @@ Isabelle.  It includes these features (amongst others):
    Script management works across multiple files for
    LEGO and Isabelle.
    
- . A toolbar for building and replaying proofs
+ . A toolbar for building and replaying proofs and interacting
+   with the proof assistant.
  
  . Syntax highlighting of proof scripts and prover output
  
@@ -73,18 +74,18 @@ Emacs gurus.
 
 To users of LEGO, Coq, and Isabelle:
 ------------------------------------
-This release of Proof General has numerous bug fixes and improvements
-over version 2.0.  It also supports the latest theorem prover
-versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99.
+Proof General 2.2 has several new features as well as bug fixes and
+improvements over versions 2.1 and 2.0.  It supports the latest
+theorem prover versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99.
 
 Please try it and let us know what you think of it!
 
-We have put a lot of work into the user documentation for Proof General 
-and making it robust and easy to install. Ideally you should
-use it with XEmacs, but it also works with limited features in 
-FSF GNU Emacs. We have tested on XEmacs 20.4,21.1 and 
-Emacs 20.2, 20.3. (It probably works with earlier versions of 
-either Emacs but we cannot guarantee this).
+We have worked hard on the user documentation, and on making Proof
+General robust and easy to install. Ideally you should use it with
+XEmacs, but it also works with limited features in FSF GNU Emacs. 
+
+We have tested on XEmacs 21.1 and Emacs 20.2, 20.3. (It probably works
+with earlier versions of either Emacs but we cannot guarantee this).
 
 
 To users of other proof assistants:
@@ -125,11 +126,11 @@ facilities (a basis already exists for LEGO), and a theory browser.
 Apart from proof assistants, script management makes sense for many
 other systems or languages with an interactive shell-like interpreter.
 We would be interested to hear from any Emacs developers interesting
-in using Proof General's script management for development in Lisp,
+in adapting Proof General's script management for development in Lisp,
 SML, or other languages.
 
 
  -- David Aspinall <da@dcs.ed.ac.uk>
-    August 1999.
+    November 1999.
 
 
diff --git a/todo b/todo
index 54e94bf5..d1407c24 100644
--- a/todo
+++ b/todo
@@ -71,16 +71,20 @@ C Internal improvements for marking up proof assistant output.
     characters.  
     Maybe using x-symbol would give another approximation, too, although
     I'm put off that because it's not so standardly a part of XEmacs yet.
+    Or maybe w3's code for HTML mark up could be borrowed.
 
 C Usability enhancement:
    Enable toolbar in other PG buffers.  Should switch to active
    scripting buffer first if it is non current.
-   (In fact, a sensible subset of scripting commands would
-    work from other buffers).
+   In fact, a sensible subset of scripting commands would
+   work from other buffers.
+   This suggestion is based on observation of a user's
+   confusion when the toolbar disappears from other PG buffers.
 
 X Compatibility enhancement:
     - Consider sending comments to proof process after all.  They might
       contain special (e.g. LaTeX) directives or something.
+      Probably only worth considering if/when it becomes a problem.
 
 A Usability enhancement:
    Movement of point after assert/retract commands
@@ -92,33 +96,33 @@ A Usability enhancement:
    Optional argument to delete region should be removed 
    from C-c C-u, pressing quickly in succession can delete
    from buffer
-B
- Usability enhancement:
+
+B Usability enhancement:
    Rationalize next and undo.  Make same as toolbar 
    commands and have different commands for power users
    to assert/retract until point.
+   At the moment this is done by binding to the toolbar
+   commands, we need to remove these from proof-toolbar now.
 
-A Usability enhancement:
+B Usability enhancement:
    Have toolbar button/command to goto a point.
    Proof General itself should work out whether it's a 
    retraction or advancement!
 
-A Usability enhancement:
-   Add toolbar button for interrupting.
-
 B Web pages: improve screenshots section to include a slideshow, or
   at least, a series of pictures of PG in action.  (3 hours)
 
 C Nicety enhancement:
-    Add messages "retracting buffer ... done" "processing ... done".
-    This needs some call backs or setting of variables examined
-    by proof-done-{advancing,retracting}
+   Add messages "retracting buffer ... done" "processing ... done".
+   This needs some call backs or setting of variables examined
+   by proof-done-{advancing,retracting}
 
 D bug: outline mode when proof-strict-read-only is nil ought to
   work, but there may be problems.
 
 D bug: mentioned by Martin H. with Lego: "don't know what I should
-  be doing..." error when it shouldn't happen.
+  be doing..." error when it shouldn't happen.  
+  [this item is useless without a more detailed description]
 
 C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
   ELISP_DIRS somehow.