Updated.

4 files changed, 18 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 7cb64b15..9fc3a113 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,12 @@
 
 ** Generic changes
 
+*** Bundling of X-Symbol Mode (4.45 beta)
+
+    !!THIS IS WORK IN PROGRESS, IT MAY WELL BREAK X-SYMBOL FOR YOU!!
+    To disable use of the bundled version, simply delete or move away
+    the x-symbol subdirectory.
+
 *** Bundling of MMM Mode (for multiple modes in one buffer)
 
     MMM mode allows submodes to be used in the same file.
diff --git a/README b/README
index 491f3550..53eeb8f0 100644
--- a/README
+++ b/README
@@ -3,8 +3,8 @@ Proof General --- Organize your proofs!
 
 Proof General is a generic Emacs interface for proof assistants.
 
-This is version 3.4 of Proof General.   
-(Check the About screen for a precise version number).
+This is version 3.5pre of Proof General.   
+(Check About screen for a precise version number; also see CHANGES).
 
 The aim of the Proof General project is to provide a powerful and
 configurable interfaces which help user-interaction with interactive
diff --git a/mmm/README.ProofGeneral b/mmm/README.ProofGeneral
index 55a36b36..ad4f9dca 100644
--- a/mmm/README.ProofGeneral
+++ b/mmm/README.ProofGeneral
@@ -2,8 +2,9 @@ The code in this directory is taken from
 
 	http://mmm-mode.sourceforge.net/
 
-This is version 0.4.7.
-No changes have been made for Proof General. 
+This is version 0.4.7.  
+No changes have been made for Proof General.   
+Some files have not be included here.
 
 
 =================================================================
diff --git a/todo b/todo
index 99720d67..d15e738e 100644
--- a/todo
+++ b/todo
@@ -7,20 +7,18 @@ This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
 * Proof General Short List of Things to Do for next version
 
 *** Clean up X-symbol support
-     -- configuration for latest version of X-Symbol (Gerwin Klein)
+     -- token configuration for latest version of X-Symbol (Gerwin Klein)
      -- remove on/off setting for all buffers (too slow), use
-        same mechanism as proof-mmm.
+        same mechanism as proof-mmm. [Done; in testing]
 
 *** Finish/cleanup MMM support for Isar.  Document (but who reads it?)
     Add MMM for other provers where relevant
 
-*** Behaviour of X-Symbol and MMM options
-      -- should have "global" behaviour, but apply to future?
-      -- just have local behaviour, add extra option for global?
-      [confusion is that particular buffer may be different from global]
-      -- does it make sense simply to synchronize global with local
-	 whenever local is changed?  
-	  [maybe: turn it off, stays off in new buffers]
+*** Isabelle support: can we somehow add "legacy" support for old 
+      theory files and even allow scripting in ML files?   Maybe
+      not, if this is even beyond what Isar interface would allow
+      (unless we send an ML file line-by-line with ML_command?)
+
  
 * Proof General Infeasibly Long Low-Level List of Things to Do