Development version becomes 3.1.

1 files changed, 3 insertions, 190 deletions

diff --git a/CHANGES b/CHANGES
index 709820a8..abea57a4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,153 +1,21 @@
-Summary of Changes for Proof General 3.0 from 2.1
+Summary of Changes for Proof General 3.1 from 3.0
 =================================================
 
+[ No changes yet, this release is the same as the stable 3.0 version ]
+
 Generic Changes
 ---------------
 
-* The excellent X-Symbol package is now well supported by
-  Proof General.  This allows proof assistants to display logical
-  symbols, Greek letters, etc, with ease.  The original patches
-  for Isabelle are courtesy of David von Oheimb.  There are
-  early experimental configurations provided for LEGO and Coq
-  which use ordinary character sequences rather than escaped
-  tokens (so "/\" appears as a wedge, and "Gamma" appears 
-  as the letter Gamma).  You may need to install X-Symbol first;
-  visit http://www.fmi.uni-passau.de/~wedler/x-symbol
-
-* Demonstration instance of Proof General for Isabelle shows
-  how you can get the interface going with a minimum of fuss.
-  It has less than 30 simple settings.
-
-* Proof General is now more cany about the queue of commands.
-  You can now add more proof commands on the end of the queue,
-  without the "Proof Process Busy" message.
-
-* New function C-c C-f (proof-find) to invoke some prover-specific
-  mechanism to search for theorems.  
-
-* Whenever scripting is triggered in a new file, a cd command
-  is sent to the proof assistant to switch to the right directory
-  (in case other files are included).
-
-* [XEmacs only] Toolbar has six new buttons (State, Context, Info, 
-  Command, Help, Stop) which invoke commands previously available on 
-  keys/menus.   Also a new "Find" button for proof-find.
-
-* [XEmacs only] Toolbar enablers have been added.   
-  Buttons are automatically enabled or disabled as appropriate.   
-  This requires XEmacs 21 or better for reliable working,
-  so is disabled for earlier versions.
-  If you do not like enablers, you can turn them off with
-  the new configuration variable proof-toolbar-use-enablers.
-  With this variable nil, buttons do nothing when they 
-  otherwise be disabled.
-
-* Menus and keybindings have been reorganized.  
-  Bindings C-c <letter> are being phased out; they are supposed
-  to be reserved for the user according to Emacs convention.
-
-* Keybindings for assert/retract now 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 !)
-
-* New command C-c C-RET proof-goto-point which generalises
-  previous proof-assert-until-point to also do retracting if
-  point is in the locked region. 
-
-* User options have been re-organized and renamed to be
-  more suggestive.  Boolean options can be
-  toggled from the menu and saved with "Save options"
-  on the ordinary Emacs "Options" menu.  (Others can
-  be set via Customize).
-
-* "Active terminator minor mode" is now called "electric 
-  terminator".   It has one setting for all buffers, and
-  you can customize it if you want it permanently on.
-
-* Command C-c C-t (proof-try-command) removed in favour of 
-  C-c C-v (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 
-
-* [XEmacs only]
-  New function control-button1 (proof-mouse-track-insert) copies 
-  individual commands (highlighted regions) from an open proof.  
-  When a proof is closed, it behaves as mouse-track-insert
-  (the default XEmacs behaviour of control-button1).  
-
-* Switching scripting buffers is now more flexible.
-  When scripting is turned off in a partly-finished buffer,
-  the user is prompted whether to retract or process the buffer.
-  Automatic retraction or completion can be selected by 
-  configuring the option proof-auto-action-when-deactivating-scripting.
-  (To be compatible with the file operations in a proof assistant,
-   Proof General only allows completely processed or completely
-   unprocessed scripts in non-active buffers).
-
-* New function C-c C-s (proof-toggle-active-scripting) to switch
-  scripting on or off in current buffer.  This is a handy way to
-  discard or finish off scripting in an unfinished buffer
-  triggering the deactivation mechanism mentioned above.
-  Switching on scripting in a buffer may cause the proof
-  assistant to load files it depends on, so it is also handy
-  to see what happens before scripting begins in the buffer.
-
-* Proof by pointing has been re-enabled in the code.  
-  LEGO's implementation of the proof-by-pointing rule choices
-  is dodgy, but works sometimes, and it is nice to demonstrate
-  Proof General's support for pbp until another prover implements
-  it.  (It should be relatively straightforward to implement for Coq,
-  since the CtCoq pbp code is now embedded in the core system; we need
-  a Coq expert to do this).
-
-* Cleaned up example files so all demonstrate same theorem "conj_comms".
-  Would be nice to add more theorems to compare scripts/proofs in
-  different systems.  Please send in example scripts!
-
-* Shorter buffer names for convenience.
- 
-* Removed transparent gif (text logo) from splash screen 
-  because XEmacs can't display it nicely.
- 
-* Documentation updates.
-
-
 Coq Changes
 -----------
 
-* Set proof-{qed,save}-commands so the toolbar functions work.
-
-* Generic command C-c C-f (proof-find-theorems) replaces Coq
-  specific command C-c C-s (coq-Search).
-
-
 LEGO Changes
 ------------
 
-* Proofs which have no save command are now closed off automatically
-  when another command arrives, so undo-redo is more flexible.
-
 
 Isabelle and Isar Changes
 -------------------------
 
-* Several tweaks for input syntax.  
-
-* Recognize goals of the old form val prems = goal ...
-  and saves of the old form val thm = result.
-
-* Proofs which are "unfinished", i.e. have no qed or result,
-  are now closed off automatically, mirroring the behaviour 
-  of Isabelle.  This does not apply to Isar.
-
-* Confusing display of only last error is fixed: multiple
-  error messages are now coalesced properly.
-
-
 Only in the developers' release
 -------------------------------
 
@@ -159,58 +27,3 @@ Only in the developers' release
 Internal changes for developers to note
 ---------------------------------------
 
-* x-symbol support has been made generic.  See documentation
-  and proof-config.el.
-
-* 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.
-
-* A new setting proof-completed-proof-behaviour allows for
-  more flexible ways of managing goal...save regions, including
-  automatically closing them when the first command after
-  the proof is completed arrives.  This means we can handle
-  proof assistants which do not have an explicit save command
-  now.   See the documentation of proof-completed-proof-behaviour.
-
-* Renamed several configuration variables for uniformity.  
-  Check the ChangeLog for details.
-
-* Speed optimizations for the proof-shell-filter, to attempt
-  to give more CPU to a hungry and noisy proof process.
-  To help with this there is a new configuration variable 
-  proof-shell-eager-annotation-start-length.
-
-* proof-site now does nothing if it has already been loaded.
-  Previously it would load again, possibly altering settings.
-
-* Multiple file handling improvements:
-   Added proof-shell-inform-file-processed-cmd setting to 
-   tell the prover about files which are processed completely 
-   inside Proof General.
-   This is called when scripting is turned off inside a completely
-   processed buffer.
-   Added proof-shell-inform-file-retracted-cmd setting for
-   symmetric case: to tell the prover when files which are to be
-   considered *not* completely processed inside Proof General.
-   The is called when scripting is turned on inside a completely
-   processed buffer (as the conceptual state of the buffer changes
-   to partly-processed).
-
-* 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
-  font-lock.  Such characters are removed from display in the
-  output buffers.  
-  However, it is NOT recommended to use this mechanism heavily,
-  because the entire mechanism of using 8 bit character codes as 
-  "special" characters is fragile and needs replacing in future
-  versions of Proof General!
-
-* proof-font-lock-zap-commas has been added to control whether
-  or not the excrutiating font-lock hack to unhighlight commas
-  is enabled.
-
-* Many code cleanups and improvements.
-