Updates

2 files changed, 29 insertions, 31 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e889a383..d3bce47f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1112,7 +1112,6 @@ The user is prompted for an argument.
 @kindex C-c c
 @kindex C-c h
 @kindex C-c C-c
-@kindex C-c t
 @kindex C-c C-v
 @kindex C-c C-f
 
@@ -1126,12 +1125,12 @@ from a proof script.  Here are the keybindings and functions.
 @code{proof-ctxt}
 @item C-c h
 @code{proof-help}
+@item C-c C-f
+@code{proof-find-theorems}
 @item C-c C-c
 @code{proof-interrupt-process}
 @item C-c C-v
 @code{proof-execute-minibuffer-cmd}
-@item C-c C-f
-@code{proof-find-theorems}
 @end table
 
 @c TEXI DOCSTRING MAGIC: proof-prf
@@ -1153,11 +1152,6 @@ Typically, a list of syntax of commands available.
 Issues a command to the assistant from @code{proof-info-command}.
 @end deffn
 
-@c TEXI DOCSTRING MAGIC: proof-interrupt-process
-@deffn Command proof-interrupt-process 
-Interrupt the proof assistant.  Warning! This may confuse Proof General.
-@end deffn
-
 @c TEXI DOCSTRING MAGIC: proof-find-theorems
 @deffn Command proof-find-theorems arg
 Search for items containing a given constant.@*
@@ -1165,6 +1159,11 @@ Issues a command based on @var{arg} to the assistant, using @code{proof-find-the
 The user is prompted for an argument.
 @end deffn
 
+@c TEXI DOCSTRING MAGIC: proof-interrupt-process
+@deffn Command proof-interrupt-process 
+Interrupt the proof assistant.  Warning! This may confuse Proof General.
+@end deffn
+
 @c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd
 @deffn Command proof-execute-minibuffer-cmd 
 Prompt for a command in the minibuffer and send it to proof assistant.@*
@@ -1174,10 +1173,10 @@ Warning! No checking whatsoever is done on the command, so this is
 even more dangerous than @code{proof-try-command}.
 @end deffn
 
-As if the last few commands weren't dangerous enough, there's also a
-command which explicitly adjusts the end of the locked region, to be
-used in extreme circumstances only.  @xref{Working directly with the
-proof shell}.
+As if the last two commands weren't risky enough, there's also a command
+which explicitly adjusts the end of the locked region, to be used in
+extreme circumstances only.  @xref{Working directly with the proof
+shell}.
 
 @c Perhaps, don't explain C-c C-z here. Instead refer to @pxref{Working
 @c directly with the proof shell}
@@ -1229,11 +1228,10 @@ This simply kills the @code{proof-shell-buffer} relying on the hook function
 @chapter Advanced Script Management
 @cindex Multiple Files
 
-What we really mean by @emph{advanced} is that Proof General supports
-large proof developments. These are typically spread across various
-files which depend on each other in some way. Proof General knows enough
-about the dependencies to allow script management across multiple files.
-
+By @emph{advanced} we mean script management for large proof
+developments. These are typically spread across various files which
+depend on each other in some way. Proof General knows enough about the
+dependencies to allow script management across multiple files.
 
 @menu
 * Switching between proof scripts::  
@@ -1412,7 +1410,7 @@ The packages currently supported are @code{font-lock} @code{func-menu},
 @vindex isa-mode-hooks
 @cindex font-lock 
 @cindex colour
-In XEmacs, proof script buffer are coloured (fontified as they say)
+In XEmacs, proof script buffers are coloured (fontified as they say)
 by default. To automatically switch on fontification in FSF GNU Emacs 20.2,
 you need to configure the @code{font-lock} package yourself. This can be
 achieved by modifying the @var{prover}-mode-hooks where @var{prover} is either
diff --git a/todo b/todo
index d1407c24..1e8303d8 100644
--- a/todo
+++ b/todo
@@ -25,8 +25,8 @@ $Id$
 ============
 
 A  (URGENT) to be fixed immediately for next pre-release 
-B           to be fixed before next release (Version 2.1)
-C           would be nice to fix before release of 2.1; but not crucial
+B           to be fixed before next release
+C           would be nice to fix before next release; but not crucial
 D (Medium)  desirable to fix at some point
 X (Low)     probably not worth spending time on
 
@@ -48,7 +48,7 @@ A Pending work, in progress [da]:
     - investigate bug fix for vacuous locked regions
     - document proof-mouse-track-insert (new name for proof-send-span, re-enabled).
 
-C Usability enhancement:
+D Usability enhancement:
     - Fix asymmetry between "doing" and "undoing": doing will skip comments,
       undoing will not.  e.g. test case: (* tester *) intros; 
 
@@ -56,7 +56,7 @@ C Usability enhancement:
     - Fix proof-script-command-separator and proof-one-command-per-line flag,
       document them.
 
-C Internal improvements for marking up proof assistant output.
+D Internal improvements for marking up proof assistant output.
     We need a better mechanism for allowing "invisible" mark up
     of assistant output based on annotations.  Present code
     allows proof-shell-leave-annotations-in-output=t to work
@@ -73,7 +73,7 @@ C Internal improvements for marking up proof assistant output.
     I'm put off that because it's not so standardly a part of XEmacs yet.
     Or maybe w3's code for HTML mark up could be borrowed.
 
-C Usability enhancement:
+D 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
@@ -86,25 +86,20 @@ X Compatibility enhancement:
       contain special (e.g. LaTeX) directives or something.
       Probably only worth considering if/when it becomes a problem.
 
-A Usability enhancement:
+C Usability enhancement:
    Movement of point after assert/retract commands
         - configure by default for one command/line.
 	- Add option for many commands per line.
 	- Maybe shell like behaviour with pressing return?
 
-A Usability enhancement:
-   Optional argument to delete region should be removed 
-   from C-c C-u, pressing quickly in succession can delete
-   from buffer
-
-B Usability enhancement:
+C Usability enhancement:
    Rationalize next and undo.  Make same as toolbar 
    commands and have different commands for power users
    to assert/retract until point.
    At the moment this is done by binding to the toolbar
    commands, we need to remove these from proof-toolbar now.
 
-B Usability enhancement:
+C Usability enhancement:
    Have toolbar button/command to goto a point.
    Proof General itself should work out whether it's a 
    retraction or advancement!
@@ -527,6 +522,11 @@ X proof-site (da): I think it would be nice to change the architecture
 X Support a history of proof commands, with a "redo" command to
   redo undo-to-point or sequences of toolbar undo's.
 
+C Support an extended version of dynamic abbreviations, to work
+  for commands rather than words.  Should behave a bit like a history
+  mechanism in shell buffer: use M-n M-p to scroll up and down
+  through previous and forthcoming (matching) commands.
+
 X Provers with sophisticated/configurable syntax should tell Emacs
   about their syntax somehow, rather than trying to duplicate
   specifications inside Emacs.