Updated

2 files changed, 32 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index 6ed6fa64..ac4cf9de 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,10 +6,14 @@
 
 *** Visibility control for completed proofs
 
-     You can make proofs invisible using a context sensitive menu
-     (right button on a completed proof), or as soon as they are
-     completed with the "Options -> Disappearing Proofs" option.
-     Two menu items "Show proofs" and "Hide proofs" apply to
+     You can make proofs invisible using a command from a new
+     context sensitive menu (XEmacs only; right button on a completed 
+     proof), or as soon as they are completed with the 
+     "Options -> Disappearing Proofs" option.
+
+     This function is also bound to C-c v (pg-toggle-visibility).
+
+     Two main-menu items "Show proofs" and "Hide proofs" apply to
      all the completed proofs in the buffer.
 
      NB: proofs of theorems with the same name are not 
@@ -46,8 +50,10 @@
  
      In this release, the experimental features are: 
 
-        Context menu options to move spans up/down
-        Context menu dependency commands (Isabelle only, see below)
+        Context menu options to move spans up/down 
+          (Only reliable in XEmacs; also on keys control-meta-up, control-meta-down)
+        Context menu dependency commands 
+          (Isabelle only, see below)
 
      To customize this from the menu:
   
@@ -87,6 +93,9 @@
      Fixed Emacs-confusion minibuffer contents switching bug.  (Bug 
      was triggered by using toolbar while minibuffer active).
 
+     Fixed problem with C-x C-v not adding completed files to included
+     files list (it does now).  
+
 ** Coq Changes
 
      Compatibility for V7 added.
diff --git a/todo b/todo
index 014e0701..ea5e72d5 100644
--- a/todo
+++ b/todo
@@ -32,9 +32,16 @@ X (Low)		e.g. probably not worth spending time on
 
 ** 2. Things to in the generic interface
 
+FOR 3.3:
+
+*** A Fix movement commands
+
+*** A Doc visibility controls
+
+====================
+
 *** C Fix byte compilation
-      Problem with proof-ass macro mechanism -- gets expanded during
-      compilation.
+      Problem with proof-ass macro mechanism -- gets expanded during compilation.
 
 *** C The PG isabelle-completion-table seems to be subject to case-fold, which
       it shouldn't be: \<sqinter> does not work, but \<Sqinter> is OK.
@@ -44,7 +51,8 @@ X (Low)		e.g. probably not worth spending time on
 *** B generalize from Isabelle's "atomic scripting" theory file mode
       to allow other instances which do not allow incremental
       processing of files in major or auxiliary file types.
-      E.g. twelf ACL2
+      E.g. twelf ACL2.
+      Also, add the atomic scripting handling for Isabelle/Isar.
 
 *** B Move over to new better designed parsing function mechanism.
 
@@ -84,11 +92,6 @@ X (Low)		e.g. probably not worth spending time on
 
 *** B Continue programme of making adaptation easier.  
 
-*** B C-x C-v does not seem to run kill buffer hooks properly: at
-  least, what happens is buffer name changes to **lose** and
-  (e.g.) a completely processed file doesn't get added to the
-  included files list.  Auto retraction appears to work.
-
 *** C Fix up sources to conform to library header conventions 
   see (lispref)Library Headers.
 
@@ -830,6 +833,12 @@ X (Low)		e.g. probably not worth spending time on
 
 ** 8. Bugs in other software beyond our control
 
+*** X Code for find-alternate-file has annoying habit of nullifying
+    buffer-file-name before kill functions are called, on a buffer
+    named ** lose **.  This means PG has to keep a copy of the
+    buffer file name to handle proof-included-files-list nicely.
+    Would be better if (X)Emacs code didn't do this.
+
 *** X useful if call-process would keep last error state 
       (primarily for exec-to-string, in case of errors)