Updated.

2 files changed, 26 insertions, 34 deletions

diff --git a/CHANGES b/CHANGES
index 30b22790..573870b2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,21 +6,26 @@
 
 *** Support for Speedbar and Index menu ("Imenu")
 
-Imenu is an alternative to Function Menu (which is described in the
-Proof General manual).  It displays a menu of named definitions,
-theorems, etc, in the file and allows quick navigation to them.
+Imenu is an alternative to Function Menu (which has been supported for
+some time, but is not built-in to GNU Emacs).  It displays a menu of
+named definitions, theorems, etc, in the file and allows quick
+navigation to them.
 
 Speedbar displays a file tree in a separate window on the display,
 allowing quick navigation.  Middle/double-clicking or pressing + on a
 file icon opens up to display tags (definitions, theorems, etc) within
 the file.  Middle/double-clicking on a file or tag jumps to that file/tag.
 
-To use Imenu, select Proof General -> Options -> Index Menu.
+To use Imenu, select Proof General -> Options -> Index Menu.  This adds
+an "Index" menu to the main menu bar.  You can also use M-x imenu for
+keyboard-driven completion.
 
 To use Speedbar, use Tools -> Display Speedbar (GNU Emacs), or
 Proof General -> Advanced -> Speedbar (XEmacs).  Or if you prefer
 the old fashioned way, `M-x speedbar' does the same job.
 
+For more about Speedbar, see http://cedet.sourceforge.net/speedbar.shtml
+
 *** Improved display management
 
 The display handling functions have been overhauled to cope with
diff --git a/todo b/todo
index 26de88cf..037e0093 100644
--- a/todo
+++ b/todo
@@ -11,39 +11,15 @@ This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
 
 *** Fixup HTML on mailing list pages
 
-*** Display management improvement (ongoing; it's a nightmare)
-    Glitches to resolve:
-     -- with multiple frame mode, new frames get selected on creation
-        (solution: create them eagerly when mode is activated).
-     -- code to delete frames isn't working
-     -- suggestion to cache window height: could implement this
-	by resize change functions (also doing the pretty-print hack?)
-        which set a symbol property for associated buffer symbol
-     -- longer term improvements: allow window preferences per 
-	associated buffer.  Either separate frame or merged into
-	switching mode.  
-     -- Stuck-withs: XEmacs frames always have minibuffer.
-		     GNU Emacs frames always have modelines.
-
 *** Update documentation.  
 
 *** Emacs Bug Roundup
     --- xemacs support for nested comments??
     --- xemacs undo in read-only regions 
 
-*** Clean up X-symbol support
-     -- token configuration for latest version of X-Symbol (Gerwin Klein, done?)
-     -- Check x-symbol support in provers other than Isabelle 
-	[Coq: OK; others?]
-
 *** Finish/cleanup MMM support for Isar.  Document.
        Add MMM for other provers where relevant
 
-*** 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?)
-
 *** Isabelle tweaks
      -- theorem dependencies on spoils ordinary response buffer output
      (dependency info *after* response display loses)
@@ -55,10 +31,6 @@ This is an outline file.   Use C-c C-n, C-c C-p or menu to navigate.
     messages from Isabelle when asking it to remove files that it says
     are already removed (noticed with auto action set to process).
 
-*** Coq issues that may be problematic:
-     -- Auto-compile-vos (prob impossible to fix)
-     -- Loss of synchronisation with silent mode (?)
-
 *** Finish clean-up of web page, broken link fixes.
 
 
@@ -92,7 +64,18 @@ X (Low)		e.g. probably not worth spending time on
 
 ** 2. Things to do in the generic interface
 
-*** PGIP SUPPORT (minimal for Isabelle patch):
+*** C Further display management improvement (it's a nightmare)
+    Glitches to resolve:
+     -- suggestion to cache window height: could implement this
+	by resize change functions (also doing the pretty-print hack?)
+        which set a symbol property for associated buffer symbol
+     -- longer term improvements: allow window preferences per 
+	associated buffer.  Either separate frame or merged into
+	switching mode.  Very messy to implement.
+     -- Stuck-withs: XEmacs frames always have minibuffer.
+		     GNU Emacs frames always have modelines.
+
+*** A PGIP SUPPORT (minimal for Isabelle patch):
       -- settings with categories
 
 *** A Oddity: Weirdness with regions turning blue even though they
@@ -100,9 +83,13 @@ X (Low)		e.g. probably not worth spending time on
     Send a few regions queueing, no result from interpreter, yet sometimes
     turns blue.  Why???
 
-*** Allow empty retract action that doesn't produce new prompt
+*** C Allow empty retract action that doesn't produce new prompt
     (Noticed with HOL4).
 
+*** unify format for syntax table entries with imenu (make alist);
+    use config setting for syntax table entries everywhere rather than
+    modify-syntax-entry.
+
 *** [ Don't query save before retraction ?? ]
 
 *** C Implement optional arg to next/undo which doesn't update