Updated, mentioning new parsing function mechanisms

1 files changed, 14 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index f2570d23..c1cff785 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,18 @@
 
 ** Generic Changes
 
+*** New more efficient and generalised parsing functions
+ 
+  Also works around crash bug in xemacs-21.1.7/SuSE.
+  Fix to previous function (used by FSF Emacs) by Markus Wenzel.
+  XEmacs uses new functions which have slightly different 
+  behaviour.  If this is problematical, please report, and
+  force the use of the old function by writing:
+
+     (defalias 'proof-segment-up-to 'proof-segment-up-to-old)
+ 
+  in your .emacs file. (Warning: only during pre-release!)
+
 *** Makefile has new target "scripts" to fix paths in bash/perl scripts
 
 *** Bug fix: "next" button enabled more often.  Solaris turns off enablers.
@@ -18,7 +30,8 @@
   for provers need initialization before synchronization can be secured.
   [Developers note: LEGO needs to wait for second prompt before sync,
    whereas Isabelle managed to sync on first prompt.  Coq was best,
-   with sync set before startup, using a command line option.]
+   with sync set before startup, using a command line option.
+   That is the recommended route for new proof assistants.]
 
 *** Bug fix: script management is now more robust against C-x C-v, C-x C-w
 
@@ -46,11 +59,6 @@
   It's nicer to do this manually if you like this mode,
   using M-x proof-goto-end-of-locked.
 
-*** Efficiency improvement in parsing
- 
-  Also works around crash bug in xemacs-21.1.7/SuSE.
-  Fix by Markus Wenzel.
-
 *** Added possibility for switching prover's output on/off.
 
   Already implemented in Coq and Isabelle(/Isar).