updates

1 files changed, 93 insertions, 111 deletions

diff --git a/todo b/todo
index 1c839a98..5bdbf99f 100644
--- a/todo
+++ b/todo
@@ -45,62 +45,13 @@ A Pending work, in progress [da]:
     - investigate toolbar refresh problems
 	. extra clicks are needed (?)
     - investigate of excessive processing for large proofs
+        (on my machine, I see about a 30% 70% worse case between Xemacs and smlnj
+         for the time_use_thy in src/HOL/Real/ROOT.ML)
     - investigate bug fix for vacuous locked regions
-    - document proof-mouse-track-insert (new name for proof-send-span, re-enabled), proof-toggle-scripting, new configuration options.
+    - document proof-mouse-track-insert (new name for proof-send-span,
+re-enabled), proof-toggle-scripting, new configuration options.
+    proof-cd
 
-B Robustify and cleanup code by allowing functions in place of regexps
-  for proof-goal-command-regexp and proof-save-command-regexp.
-  New names: proof-goal-command-match, proof-save-command-match.
-  Then we can remove duplicity and simplify code.
-
-B Fix colouring of response buffer, may be broken.  The idea was
-  that the latest message would always be highlighted, I think.
-
-B Usability enhancement: remove stupid "I don't know what I should be doing"
-  errors and replace with something more informative.
-
-B Doc enhancement: explain conditions for switching buffers and auto
-  switching of scripting buffers.  (See doc of 
-  proof-auto-action-when-switching-scripting)
-
-D Multiple file improvements: add implicit
-D Usability enhancement:
-    - Fix asymmetry between "doing" and "undoing": doing will skip comments,
-      undoing will not.  e.g. test case: (* tester *) intros; 
-
-C Usability enhancement:
-    - Fix proof-script-command-separator and proof-one-command-per-line flag,
-      document them.
-
-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
-    together with font-lock to do mark up.  
-    Instead we need something more like what enriched-mode does
-    (although I've just tried it and I foound that copying with 
-    the mouse ignores the text properties, but copying with the 
-    keyboard copies them!).  It uses a general library
-    format.el for reading and writing files in multiple formats.
-    This is not quite what we want for our purpose, but it might be a
-    closer approximation than using font lock and hiding the special
-    characters.  
-    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.
-    Or maybe w3's code for HTML mark up could be borrowed.
-
-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
-   work from other buffers.
-   This suggestion is based on observation of a user's
-   confusion when the toolbar disappears from other PG buffers.
-
-X Compatibility enhancement:
-    - Consider sending comments to proof process after all.  They might
-      contain special (e.g. LaTeX) directives or something.
-      Probably only worth considering if/when it becomes a problem.
 
 C Usability enhancement:
    Movement of point after assert/retract commands
@@ -120,6 +71,8 @@ C Usability enhancement:
    Proof General itself should work out whether it's a 
    retraction or advancement!
 
+C Unify toolbar and menu functions. (1h)
+
 B Web pages: improve screenshots section to include a slideshow, or
   at least, a series of pictures of PG in action.  (3 hours)
 
@@ -128,20 +81,22 @@ C Nicety enhancement:
    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.
+C Fix colouring of response buffer, may be broken.  The idea was
+  that the latest message would always be highlighted, I think.
 
-D bug: mentioned by Martin H. with Lego: "don't know what I should
-  be doing..." error when it shouldn't happen.  
-  [this item is useless without a more detailed description]
+C Usability enhancement: remove stupid "I don't know what I should be doing"
+  errors and replace with something more informative.
 
-C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
-  ELISP_DIRS somehow.
+C Doc enhancement: explain conditions for switching buffers and auto
+  switching of scripting buffers.  (See doc of 
+  proof-auto-action-when-switching-scripting)
 
-D Update logo to include new "???" prover badge  (maybe it should be 
-  "...") from graphics file elsewhere (da)
+C Usability enhancement:
+    - Fix proof-script-command-separator and proof-one-command-per-line flag,
+      document them.
 
-D Add etc/announce to web pages somewhere.
+C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
+  ELISP_DIRS somehow.
 
 B Improve relocatability of RPM package, and produce package for XEmacs
   which installs directly under ~/.xemacs/packages.
@@ -154,12 +109,72 @@ C Check compilation okay, check on use of eval-and-compile.
 C Support for proof-guess-command-line, new generic setting added
   by Patrick.
 
+D Update logo to include new "???" prover badge  (maybe it should be 
+  "...") from graphics file elsewhere (da)
+
+D Add etc/announce to web pages somewhere.
+
 D Key binding and interface issues
   - Consider change for prefix argument for C-c C-u and C-c u,
   it's quite easy to accidently delete by pressing C-c C-u
   repeatedly.
 
-D CVS repository issues.
+D Usability enhancement:
+    - Fix asymmetry between "doing" and "undoing": doing will skip comments,
+      undoing will not.  e.g. test case: (* tester *) intros; 
+
+D Robustify and cleanup code by allowing functions in place of regexps
+  for proof-goal-command-regexp and proof-save-command-regexp.
+  New names: proof-goal-command-match, proof-save-command-match.
+  Then we can remove duplicity and simplify code.
+
+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
+    together with font-lock to do mark up.  
+    Instead we need something more like what enriched-mode does
+    (although I've just tried it and I foound that copying with 
+    the mouse ignores the text properties, but copying with the 
+    keyboard copies them!).  It uses a general library
+    format.el for reading and writing files in multiple formats.
+    This is not quite what we want for our purpose, but it might be a
+    closer approximation than using font lock and hiding the special
+    characters.  
+    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.
+    Or maybe w3's code for HTML mark up could be borrowed.
+
+X Multiple file improvements: add automatic/implict handling of 
+  multiple files, by retracting across file boundaries automatically 
+  if there is no support from the proof assistant to do this.  Idea is
+  that when we retract file B and loaded files list is A B C D E,
+  then C D E are retracted too (one by one).  Retraction should
+  happen (before) first undo takes place in a buffer on the loaded
+  files list.  Type theory proof assistants with a linear context
+  can be handled perfectly this way.
+
+X 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.
+   This suggestion is based on observation of a user's
+   confusion when the toolbar disappears from other PG buffers.
+
+X Compatibility enhancement:
+    - Consider sending comments to proof process after all.  They might
+      contain special (e.g. LaTeX) directives or something.
+      Probably only worth considering if/when it becomes a problem.
+
+X bug: outline mode when proof-strict-read-only is nil ought to
+  work, but there may be problems.
+
+X bug: mentioned by Martin H. with Lego: "don't know what I should
+  be doing..." error when it shouldn't happen.  
+  [this item is useless without a more detailed description]
+
+X CVS repository issues.
   Where are obsolete 'fileattr' files generated from/maintained?
   Should junk these (which appear to say that tms is watching everything).
 
@@ -262,7 +277,7 @@ C Improve indentation code and see why it's so slow (at
   least for Isabelle).   Enable it for particular provers if
   it works okay  (but must test in on large files).
 
-C Regions in script buffer have nice "name" property and configurers
+C Proofs in script buffer have nice "name" property and configurers
   have to set regexps carefully so that it works, but is it actually
   used anywhere?   What's it good for?
 
@@ -276,32 +291,17 @@ C support for templates e.g., in LEGO it would be nice if, by default,
   fresh buffers corrsponding to file foo.l would automatically insert
   "Module foo;" (1h)
 
-C  Remove "FIXME notes" which are just notes I've put in about old
-   code in case something breaks   (da, 10mins).
+D  Review "FIXME notes" which are notes about ongoing fixes or
+   sometimes things to do. 
 
-C  Check on all FIXME notes.
-
-C  automise testing procedures in etc/
+D  automise testing procedures in etc/
 
 C  Write proof-define-derived-mode which automatically adds a 
-   call back hook somehow.  Propose this to maintainer of derived.el.
-   (1.5hrs)
+   call back hook somehow corresponding to our "proof-config-done"
+   mess.  Propose this to maintainer of derived.el. (1.5hrs)
 
 C  Toolbar icon for `proof-execute-minibuffer-cmd'  (1.5hrs)
 
-C Improve web pages after suggestions in doc/notes.txt
-  (da, 1.5hrs)
-
-C proof-issue-goal should refuse to work when a proof is in progress.
-  Similarly proof-issue-save should refuse to work when a proof
-  hasn't been completed! Algorithm: Search the last goal and check
-  length of span.  (45min)
-
-C Bug in proof-retract-until-point when called twice in succession:
-  calls backward-char at beginning of buffer.  (Should say no
-  locked region, or "nothing to retract").  Problems is that
-  there is a proof-locked-end, but it's at (point-min). (30min)
-
 C Clean up proof-assert-until-point behaviour.  Discussion results:
     1.  At the moment we get an odd error if it is run in
     the locked region.    This is a bug.  Should behave same
@@ -331,45 +331,30 @@ C Improve proof-goal-command and proof-save-command:
 
      (setq proof-goal-command  (proof-prompt-named-goal "Goal %s :" "%s;"))
 
-C Cleanup handling of proof-terminal-string.  At the moment some
+X Cleanup handling of proof-terminal-string.  At the moment some
   commands need to have the terminal string, some don't.
   da: I suggest removing proof-terminal-string altogether and
   adding back the semi-colons or fullstops at the specific level.
   It's not a big deal and would support other provers which
   may use a mixture of terminators, or no terminators at all.
+  [Trouble with this is that terminators are used for active
+   terminator mode, among several other things]
 
-C Functions for next,previous input a la shell mode, but in proof
-  script buffer (3h, da).
+X Functions for next,previous input a la shell mode, but in proof
+  script buffer (5h, da).
 
-C User-level functions: 
-  1. add new version of undo-until-point which behaves analogously to 
-  proof-assert-next-command.
-  2. make version of proof-restart-script which will start or
-  restart the proof assistant as appropriate.  (It's handy to have
-  a direct function to start the proof assistant).
-  (1hr, da)
-
-C Write test schedule for things to try out with a new instantiation
+X Write test schedule for things to try out with a new instantiation
   of Proof General.
 
-C Add skeleton instantiation files for a dummy prover "myassistant" to
+X Add skeleton instantiation files for a dummy prover "myassistant" to
   make it easier to add support for new assistants -- looking at
   any of the existing modes is confusing because of the
   prover-specific stuff.  Ideally it should work for one of
   the default provers as an impoverished example mode.
-  (2h, da will do for Isabelle)
-
-C 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). This could be 
-  achieved with a hook which is not set by default. [Remember to add
-  user documentation] (30min)
 
 C Reengineer *-count-undos and *-find-and-forget at generic level
   (3h)
 
-C Unify toolbar and menu functions. (1h)
-
 C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's.
   Generic problem, really: maybe CRs should be stripped, and just first
   line of multiline urgent message displayed in minibuffer.
@@ -385,9 +370,6 @@ D Perhaps goal..save sequences should be closed also by the appearance
 
   Will ACS idea handle this?
 
-D Better support for adding a new prover: give error messages which
-  hint at what variable to set (see proof-issue-goal for example).
-
 D Multiple files: handle failures in reading ancestors.
 
 D Provide a sensible default frame/buffer layout (4h)