Updated

3 files changed, 39 insertions, 8 deletions

diff --git a/BUGS b/BUGS
index 71bea29d..b9fe6a6b 100644
--- a/BUGS
+++ b/BUGS
@@ -16,6 +16,10 @@ mess.  The underlying text property implementation has changed
 and it seems difficult to get the desired behaviour of highlighting
 now.   Workaround: switch to using XEmacs.
 
+* If you use C-x C-v or C-x C-w on a script file which is in active
+scripting mode, Proof General will lose track of the file.
+Workaround: always turn off active scripting first with C-c C-s.
+
 * Toolbar enablers for XEmacs 21: since these have been switched on,
 it is apparent that the recognition of completed proofs may be
 unreliable (it wasn't used before).  Also there is a timing issue,
@@ -89,6 +93,8 @@ using rsh instead, it is said to forward signals to the remote command.
 LEGO Proof General Bugs
 =======================
 
+* PBP doesn't work on FSF, see note above.
+
 * [FSF specific] `proof-zap-commas-region' does not work for Emacs
   20.2 on lego/example.l . On *initially* fontifying the buffer,
   commas are not zapped [unfontified]. However, when entering text,
@@ -99,11 +105,11 @@ LEGO Proof General Bugs
   Proof General and gets stuck. Workaround: Directly enter "Configure
   AnnotateOn" in the Proof Shell to recover.
 
-* After a `Discharge', retraction ought to only be possible back to the
-first declaration/definition which is discharged. However, LEGO Proof
-General does not know that Discharge has such a non-local effect.
-Workaround: retract back to the first declaration/definition which is
-discharged.
+* After a `Discharge', retraction ought to only be possible back to
+the first declaration/definition which is discharged. However, LEGO
+Proof General does not know that Discharge has such a non-local
+effect.  Workaround: retract back to the first
+declaration/definition which is discharged.
 
 * A thorny issue is local definitions in a proof state. LEGO cannot
 undo them explicitly. Workaround: retract back to a command before a
diff --git a/CHANGES b/CHANGES
index 48c38b71..f7ab5b75 100644
--- a/CHANGES
+++ b/CHANGES
@@ -100,8 +100,8 @@ Generic Changes
   LEGO's implementation of the proof-by-pointing rule choices
   is dodgy, but works sometimes, and it is nice to demonstrate
   Proof General's support for pbp until another prover implements
-  it.  (It should be straightforward to implement for Coq, since the
-  CtCoq pbp code is now embedded in the core system; we need
+  it.  (It should be relatively straightforward to implement for Coq,
+  since the CtCoq pbp code is now embedded in the core system; we need
   a Coq expert to do this).
 
 * Cleaned up example files so all demonstrate same theorem "conj_comms".
diff --git a/todo b/todo
index 5cc8285a..96ff2087 100644
--- a/todo
+++ b/todo
@@ -54,6 +54,14 @@ A Final stuff for 3.0 release [da]:
 
 ---------------------------------------------
 
+B Fix problems with C-x C-v and C-x C-w 
+
+B Make tags support in lego.el and coq.el a bit more generic.
+  Use customization option proof-tags-support.
+
+B Fix up sources to conform to library header conventions 
+  see (lispref)Library Headers.
+
 B Proof shell exit function -- could try sending an interrupt first
   if the process is busy, just to be polite (and avoid the 10 second
   wait before it gets killed).
@@ -73,6 +81,9 @@ B Continue program of making adaptation easier.
    - Test proof-easy-config mechanism.
    - Add proof-shell-important-settings and test that they're set.
 
+B Documentation in pdf format: need to fix inclusion of image 
+  problem.
+
 C Quit timeout enhancement: instead of killing immediately after
   timeout, could give a message "not responding, kill immediately?"
 
@@ -117,6 +128,8 @@ B Oops --- here's an alternate and better fix to Isabelle goals
   marked up as a proof state output.  This gets rid of the
   proof-goals-display-qed-message kludge.  See comments in code.
 
+C Consider supporting imenu instead, or as well as, func-menu.
+
 C Fix the sentinel infinite loop bug which occurs in some cases
   when proof shell startup fails.  Same message is printed over
   and over.  Infinite in FSF Emacs.  Why?  See note at 
@@ -147,7 +160,8 @@ C Improved configurability of command settings, etc.
   Then use a generic function "proof-invoke-function" or similar.
 
 D Consider proof-generic-goal-hyp function, for proof by
-  pointing support.
+  pointing support.  Based on `proof-shell-goal-regexp' which
+  I accidently introduced at one point.
 
 D Make code robust against accidental deletion of response/goals
   buffer.  Add functions proof-get-or-create-{response,goals}-buffer.
@@ -846,6 +860,14 @@ is 8 bit.  Suspect an XEmacs issue to do with face allocations.  Also
 huge delay in buffers for Isabelle mode which try to highlight binders
 (removed because they appear inside strings anyway)
 
+X spurious byte comp warning in XEmacs 21.1.4:
+  While compiling proof-x-symbol-encode-shell-input:
+     ** buffer-substring called with 3 args, but requires 0-3
+  for this code:
+               (prog1 (buffer-substring)
+                 (kill-buffer (current-buffer))
+
+
 
 
 
@@ -863,6 +885,8 @@ huge delay in buffers for Isabelle mode which try to highlight binders
 2. Check case with FSF Emacs
 3. Check case with compiled code, for XEmacs only.
    (Wait for error reports for FSF Emacs)
+   Even if the code is faulty afterwards, compiling is 
+   worthwhile just because it shows up bugs in unbound variables, etc.
 4. Dates and versions updated in:
      README, doc/ProofGeneral.texi, html/download.html
 5. ProofGeneral.texi docstring magic is up-to-date:
@@ -889,6 +913,7 @@ A Try to get small project grant from LFCS to help with
     - Re-engineering Proof General to use XML-style 
       markup instead of 8bit chars, and proposing a
       standard goals/pbp output scheme
+    - Fix up FSF Emacs support (character problem)
 
 A Consider writing a grant proposal related to
   Proof General to generate funding for Proof General.