*** empty log message ***

2 files changed, 65 insertions, 43 deletions

diff --git a/script-management.texinfo b/script-management.texinfo
index 3e07455b..268add70 100644
--- a/script-management.texinfo
+++ b/script-management.texinfo
@@ -28,6 +28,7 @@ support building and secure editing of proof scripts.  Currently custom
 modes exist for LEGO and Coq.
 
 @menu
+* Credits::               The people Involved
 * Introduction::          Introduction to Script Management
 * Commands::              Proof mode Commands
 * Multiple Files::        Proof developments spanning several files
@@ -40,7 +41,16 @@ modes exist for LEGO and Coq.
 * Known Problems::        Caveat Emptor
 @end menu
 
-@node Introduction, Commands, Top, Top
+@node Credits, Introduction, Top, Top
+@section Credits
+
+Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf
+Goguen, Thomas Kleymann and Dilip Sequeira have implented a generic
+proof mode for Emacs. The original proof-by-pointing algorithm has been
+implemented by Yves Bertot. This manual was originally written by Dilip
+Sequeira. 
+
+@node Introduction, Credits, Commands, Top
 @section Introduction
 
 Each script resides in an Emacs buffer, called a @emph{script buffer},
@@ -122,6 +132,15 @@ you to the active one.
 @item C-c C-e
 move the point to the next terminator
 
+@item C-c C-p
+display the proof state in the response buffer
+
+@item C-c c
+display the context in the response buffer
+
+@item C-c h
+print LEGO help text in the response buffer
+
 @item C-c C-c
 interrupt the process process. This may leave script management or the
 proof process (or both) in an inconsistent state.
@@ -326,7 +345,7 @@ goal by pointing now, but we'll stay with the keyboard.
 
 finishes the Goal. 
 
-@samp{Save;}
+@samp{Save bland_commutes;}
 
 Moving the mouse pointer over the locked region now reveals that the
 entire proof has been aggregated into a single segment. Suppose we
@@ -341,22 +360,7 @@ processing and executes them.
 @section LEGO mode
 
 LEGO mode is a mode derived from proof mode for editing LEGO scripts.
-As well as custom popup menus, it has the following commands:
-
-@table @kbd
-
-@item C-c C-p
-display the proof state in the response buffer
-
-@item C-c c
-display the context in the response buffer
-
-@item C-c c
-print LEGO help text in the response buffer
-
-@end table
-
-In addition, there are some abbreviations for common commands, which
+There are some abbreviations for common commands, which
 add text to the buffer:
 
 @table @kbd
@@ -377,16 +381,10 @@ As well as custom popup menus, it has the following commands:
 
 @table @kbd
 
-@item C-c C-p
-display the proof state in the response buffer
-
 @item C-c C-s
 search for items in the library of a given type.  This runs the
 @kbd{Search} command of Coq.
 
-@item C-c c
-display the context in the response buffer
-
 @end table
 
 In addition, there are some abbreviations for common commands, which
diff --git a/todo b/todo
index 643867a9..05ae2c3a 100644
--- a/todo
+++ b/todo
@@ -9,7 +9,9 @@ C (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-A Write function proof-retract-file. (hhg? 30min)
+A Write function proof-retract-file. (30min)
+  Currently, the command ForgetMark (for LEGO) is hardwired in
+  proof-steal-process.
 
 A Update source documentation and manual, in particular document bugs
   and workarounds
@@ -43,21 +45,18 @@ C XEmacs sessions seem to grow excessively in terms of memory
   Setting a limit on the size of the process buffer doesn't seem to
   help. 
 
-A Fixing up errors caused by pbp-generated commands; currently, script
-  management unwisely assumes that pbp commands cannot fail (2h tms)
-
-C pbp code doesn't quite accord with the tech report; in particular it
-  decodes annotations eagerly. Lazily would be faster, and it's what
-  the tech report claims
-  --- djs: probably not much faster, actually.
-
-B file handling could be more robust; perhaps one should always cd to
+A file handling could be more robust; perhaps one should always cd to
   the directory corresponding to the script buffer (currently only
   done for the buffer which starts up the proof system) (30min tms)
 
-B replace (current-buffer) by proof-shell-buffer/proof-script-buffer
+A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
   where ever possible (30 min tms)
 
+A Replace "You are not authorised for this information." by a proper
+  documentation 
+
+A Reengineer *-count-undos and *-find-and-forget at generic level
+
 B Allow bib-cite style clicking on Load/Import commands to go to file.
 
 C LEGO and Coq modes overwrite each other.
@@ -73,16 +72,36 @@ B Remove LEGO-specific code in proof.el: for example,
   proof-shell-eager-annotation-end, proof-included-files-list.
   (added by hhg)
 
+B support font-lock in response buffer
+
+B Response buffer: after an error message has been displayed; ensure
+  that the error message is visible
+
+B Introduce keybinding to save the proof e.g., in LEGO, this should
+  insert "Save id" or "$Save id" depending on the name of the theorem. 
+
+* Proof-by-Pointing
+===================
+
+A Fixing up errors caused by pbp-generated commands; currently, script
+  management unwisely assumes that pbp commands cannot fail (2h tms)
+
+A Rename pbp-mode to response-mode (which doesn't support any actual
+  proof-by-pointing)  
+
+A Outsource actual pbp functionality
+
+C pbp code doesn't quite accord with the tech report; in particular it
+  decodes annotations eagerly. Lazily would be faster, and it's what
+  the tech report claims
+  --- djs: probably not much faster, actually.
+
 * Here are things to be done to Lego mode
 =========================================
 
-A set up regular definitions to support definitions of the form
-  id == term (10min; tms)
-
 A fix Pbp implementation (10h; tms)
 
-A LEGO mode might incorporate changes to Coq mode menu, in particular
-  making help refer to the info file (30min tms)
+A Implement menu at generic level. (30min tms)
 
 A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
   annotations are recorded in the object file. This needs to be
@@ -90,7 +109,7 @@ A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
 
 C Mechanism to save object file
 
-A Equiv, Next,... aren't handled properly, because LEGO does not
+B Equiv, Next,... aren't handled properly, because LEGO does not
   refresh the proof state. Perhaps it would be easiest to get LEGO to
   output more information in proof script mode (2h tms)
 
@@ -132,6 +151,11 @@ B The proof-locked-span isn't set to read-only, because overlays don't
   have that capability.  This needs to be done with text-regions.
   (2hr hhg)
 
-B Replace running-(xemacs|emacs19) in proof.el by fboundp. (20min tms)
+* Release
+=========
+
+A remove CVS history in all files
+
+A extend Copyright to 1998
 
-A Replace recursion with while-loop in span-overlay. (2h hhg)
+A Release Number 2.0
\ No newline at end of file