Updated.

2 files changed, 23 insertions, 24 deletions

diff --git a/BUGS b/BUGS
index b4abf567..27c6decf 100644
--- a/BUGS
+++ b/BUGS
@@ -3,8 +3,8 @@
 * Bugs to be fixed before PG 3.5 is released; recently noted items
 
 The items below are known and will be fixed (or shifted to the list
-below) before 3.5 is released. Please don't send email about them
-(unless you can fix them).
+below) before 3.5 is released. Please don't send email about these
+(unless you can fix them).  Please do send email about others.
 
 ** Various menu problems with Emacs 21.2.
 
@@ -12,13 +12,6 @@ PG menus may be added to wrong bar during autoload.  See CHANGES for
 temporary workaround.
 
 
-** Occasional appearance of <^sync> messages in Isabelle/Isar output
-
-Due to a patch for Coq that has changed some internals.  Patch is due
-to be reverted, Coq itself has been changed to avoid need for the
-hack.  May cause other glitches with Isabelle.
-
-
 ** UTF-8 problems with Red Hat 8.0 / glibc 2.2  and (at least) Coq.  
 
 RedHat 8 has glibc 2.2 and UTF8 encoded output may be turned on in
diff --git a/CHANGES b/CHANGES
index 2c1d8055..8d8a030e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,17 @@
 
 * Summary of Changes for Proof General 3.5pre from 3.4
 
+** Generic changes
+
+*** X-Symbol (and MMM-mode) minor mode behaviour simplified
+ 
+    These minor modes like to be responsible for turning themselves
+    on and off.  PG does not anymore try to synchronise the on/off
+    settings in all PG buffers (which could lead to half an hour
+    of fontification!).  Instead the menu reflects the current
+    minor mode status; toggling it will also update the default
+    "global for PG" behaviour for new script buffers.
+
 *** Bundling and configuration for Multiple Modes (MMM-Mode)
 
     MMM mode allows submodes to be used in the same file.
@@ -15,19 +26,6 @@
     At present it is configured for Isar, to allow LaTeX and
     sml-mode to be used inside Isar scripts.
 
-
-** GNU Emacs compatibility, simplified font-lock, handling nested comments
-
-*** Numerous improvements, thanks due to Stefan Monnier.
-
-*** Some GNU Emacs backwards compatibility removed: use 21.1 or later
-
-*** PROBLEMS REMAINING: Menu problems currently on 21.2, may affect loading.
-    Temp fix: turn on mode manually first in *scratch* buffer, then
-    visit file.
-
-** Generic changes
-
 *** Follow mode: add "followdown" setting
 
 In this mode, the point moves with the locked region when it moves
@@ -62,13 +60,21 @@ do not print multiple identical prompts for continued lines.
 [this is in testing: please notify me of problems in other provers]
 
 
+** GNU Emacs compatibility, simplified font-lock, handling nested comments
+
+*** Numerous improvements, thanks due to Stefan Monnier.
+
+*** Some GNU Emacs backwards compatibility removed: use 21.1 or later
+
+*** PROBLEMS REMAINING: Menu problems currently on 21.2, may affect loading.
+    Temp fix: turn on mode manually first in *scratch* buffer, then
+    visit file.
+
 ** Changes for Isabelle
 
 Beginnings of support PGIP protocol (work in progress with Isabelle
 CVS version).  Presently allows Isabelle to configure Proof General.
 
-CURRENTLY SUPPORT FOR CURRENTLY RELEASED ISABELLE VERSIONS IS BROKEN!
-
 Backward compatibility may not be maintained: it's simply too much
 effort.  This means that if you upgrade your Emacs version, which
 forces you to upgrade Proof General because Emacs upgrades usually