Updates.

3 files changed, 26 insertions, 19 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index eca6b32f..2b005810 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -949,9 +949,11 @@ Must be an active scripting buffer.
 @node Script processing commands
 @section Script processing commands
 @kindex C-c C-n
+@kindex C-c C-u
+@kindex C-c C-b
+@kindex C-c C-r
 @kindex C-c RET
 @kindex C-c u
-@kindex C-c C-u
 
 Here are the commands for asserting and retracting portions of the proof
 script, together with their default key bindings.  Note that assertion
@@ -1024,6 +1026,10 @@ delete the retracted region from the proof-script.
 Process the current buffer and set point at the end of the buffer.
 @end deffn
 
+@c TEXI DOCSTRING MAGIC: proof-retract-buffer
+@deffn Command proof-process-buffer 
+Process the current buffer and set point at the end of the buffer.
+@end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-active-terminator-minor-mode
 @deffn Command proof-active-terminator-minor-mode &optional arg
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 3f9e2622..cfdb6e66 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1295,6 +1295,8 @@ the proof script."
   (goto-char (point-min))
   (proof-retract-until-point-interactive))
 
+
+
 ;; FIXME da: this could do with some tweaking.  Be careful to
 ;; avoid memory leaks.  If a buffer is killed and it's local
 ;; variables are, then so should all the spans which were allocated
diff --git a/todo b/todo
index 1d7c45fa..54e94bf5 100644
--- a/todo
+++ b/todo
@@ -38,33 +38,23 @@ X (Low)     probably not worth spending time on
 ====================================
 
 A Pending work, in progress [da]:
-    - new toolbar button icons 
-          (fixup eye shadows, mag glass, finger, stop icon)
-    - command and button for searching for a theorem
-       (possibly matching a given constant, or the proof state).
     - reorganization and improvement of menus, keybindings
 	. use toolbar functions, but remove from proof-toolbar and reorganize.
 	. update documentation
     - test support for x-symbol
     - investigate toolbar refresh problems
-	. extra clicks are needed
-	. toolbar appears in wrong buffers
+	. extra clicks are needed (?)
     - investigate of excessive processing for large proofs
     - investigate bug fix for vacuous locked regions
-    - bug when prover gives error from proof-find (or similar functions)
     - document proof-mouse-track-insert (new name for proof-send-span, re-enabled).
 
-A Usability enhancement:
+C Usability enhancement:
     - Fix asymmetry between "doing" and "undoing": doing will skip comments,
       undoing will not.  e.g. test case: (* tester *) intros; 
 
-A Usability enhancement:
+C Usability enhancement:
     - Fix proof-script-command-separator and proof-one-command-per-line flag,
-    document them.
-
-C Compatibility enhancement:
-    - Consider sending comments to proof process after all.  They might
-      contain special (e.g. LaTeX) directives or something.
+      document them.
 
 C Internal improvements for marking up proof assistant output.
     We need a better mechanism for allowing "invisible" mark up
@@ -82,12 +72,16 @@ C Internal improvements for marking up proof assistant output.
     Maybe using x-symbol would give another approximation, too, although
     I'm put off that because it's not so standardly a part of XEmacs yet.
 
-A Usability enhancement:
-   Enable toolbar in other buffers.  Should switch to active
+C Usability enhancement:
+   Enable toolbar in other PG buffers.  Should switch to active
    scripting buffer first if it is non current.
    (In fact, a sensible subset of scripting commands would
     work from other buffers).
 
+X Compatibility enhancement:
+    - Consider sending comments to proof process after all.  They might
+      contain special (e.g. LaTeX) directives or something.
+
 A Usability enhancement:
    Movement of point after assert/retract commands
         - configure by default for one command/line.
@@ -98,8 +92,8 @@ A Usability enhancement:
    Optional argument to delete region should be removed 
    from C-c C-u, pressing quickly in succession can delete
    from buffer
-
-A Usability enhancement:
+B
+ Usability enhancement:
    Rationalize next and undo.  Make same as toolbar 
    commands and have different commands for power users
    to assert/retract until point.
@@ -115,6 +109,11 @@ A Usability enhancement:
 B Web pages: improve screenshots section to include a slideshow, or
   at least, a series of pictures of PG in action.  (3 hours)
 
+C Nicety enhancement:
+    Add messages "retracting buffer ... done" "processing ... done".
+    This needs some call backs or setting of variables examined
+    by proof-done-{advancing,retracting}
+
 D bug: outline mode when proof-strict-read-only is nil ought to
   work, but there may be problems.