Reorganized.

1 files changed, 47 insertions, 56 deletions

diff --git a/todo b/todo
index c7005223..33bc8191 100644
--- a/todo
+++ b/todo
@@ -14,25 +14,6 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-C  proof-goal-command-regexp: add this setting to coq.el.
-   Rationalize use of proof-goal-command-p
-   (probably can be scrapped now).  
-
-D  Customization mechanism: is there a way to make saved settings
-   not be overwritten by setq's in the code?  Need to think how
-   to do this, something like customize-set-variable-if-unchanged
-   Otherwise no so useful for people to use customize for
-   prover config settings (we'd need to shadow them all again for
-   each assistant for this to work smoothly).
-   Sure sign saving will fail is when you see "this option has
-   been changed outside customization buffer"
-
-C Customization mechanism and config variables: at the moment even
-  setting config variables in a hook is tricky, because
-  proof-config-done is called before the hook variables for the
-  new mode are.  Our new version of define-derived-mode needs
-  to address this.
-
 A* multiple files bug fix:
    It can happen (in Isabelle) that the prover retracts a file
    which asks for another to be retracted which is *not* on
@@ -44,6 +25,17 @@ A* multiple files bug fix:
    --> One case now fixed by allowing current scripting buffer to
     be retracted.  Are there other cases?  (da to investigate)
 
+A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
+  Technical Report (2+2 days; da + tms)
+
+A Check that byte compilation (and compiled code!) 
+  works for both varieties of Emacs. 
+  Fill out Makefile.dist (2hr da)
+
+C  proof-goal-command-regexp: add this setting to coq.el.
+   Rationalize use of proof-goal-command-p
+   (probably can be scrapped now).  
+
 C  Strange behaviour when killing and re-visiting files that
    haven't been completely processed.  Since they stay on
    the proof-included-files-list, on re-visiting, they are
@@ -60,11 +52,6 @@ C  The semantics of `proof-script-buffer-list' is ambigous. The first
    dynamically if a buffer is instrumented for scripting, contains a
    locked region, etc. (4h, including testing)
 
-A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
-  Technical Report (2+2 days; da + tms)
-
-A* Bug in proof-mode configuration of func-menu.  (30mins)
-
 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).
@@ -73,11 +60,6 @@ C Regions 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?
 
-B Proofs in Isabelle scripts can be non-interactive.  Non-interactive
-  proofs have only one command.  We need to find a way to integrate
-  these into Proof General nicely.  Perhaps things would work
-  fine simply if these match save goal forms?  (da, 1hr)
-
 C ROBUSTness: deal gracefully with possibility that goals buffer is
   killed during session.   (2h)
 
@@ -91,17 +73,15 @@ B da: goal-hyp: this should be more generic.  At the moment, there are
 D Add support to filter out unwanted noise from the prover by setting
   up a regular expression  proof-shell-noise-regexp (1h)
 
-A Check that byte compilation (and compiled code!) 
-  works for both varieties of Emacs. 
-  Fill out Makefile.dist (2hr da)
-
 B Make completion more generic. For Isabelle and Lego, we can build a
   completion table by querying the process, which is better than
   messing with tags.  
 A* fix any bits I've broken  (da, 1hr)
 
-B Add menu function to switch to proof shell buffer, goals buffer,
-  response buffer and current proof script buffer. (30min)
+B Add proof-quit-command: some provers may like a quit command to be
+  sent to the shell, not just EOF !  (see proof-stop-shell).
+  Also reconcile proof-restart-script and proof-stop-shell, see
+  comments in code. (1h da)
 
 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
@@ -140,14 +120,6 @@ C Bug in proof-retract-until-point when called twice in succession:
   locked region, or "nothing to retract").  Problems is that
   there is a proof-locked-end, but it's at (point-min). (30min)
 
-B Add proof-quit-command: some provers may like a quit command to be
-  sent to the shell, not just EOF !  (see proof-stop-shell).
-  Also reconcile proof-restart-script and proof-stop-shell, see
-  comments in code. (1h da)
-
-D Multiple files: handle failures in
-  reading ancestors.
-
 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
@@ -166,8 +138,6 @@ C Clean up proof-assert-until-point behaviour.  Discussion results:
     when new commands are added to the buffer needs careful
     thought! (1h)
 
-D Provide a sensible default frame/buffer layout (4h)
-
 C A less drastic version of proof-restart-script would be useful:
   one that doesn't involve killing off the proof assistant process
   and restarting that -- it can take ages! 
@@ -224,6 +194,21 @@ C Add skeleton instantiation files for a dummy prover "myassistant" to
   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)
+
+D Multiple files: handle failures in reading ancestors.
+
+D Provide a sensible default frame/buffer layout (4h)
+
 D Implement mouse drag-and-drop support for selecting subterms in the
   goals buffer and copying them in a script buffer. This could be
   implemented by defining button2 in the response buffer and setting
@@ -238,22 +223,28 @@ D Add support to proof.el for *not* setting variables for
 D Implement proof-find-previous-terminator and bind it to C-c C-a
   (45min)
 
-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)
-
 D Allow bib-cite style clicking on Load/Import commands to go to file.
 
-C Unify toolbar and menu functions. (1h)
-
 D Remove duplication of variables e.g., proof-prog-name and
   lego-prog-name for Coq and Lego. (1h)
 
+X  Customization mechanism: is there a way to make saved settings
+   not be overwritten by setq's in the code?  Need to think how
+   to do this, something like customize-set-variable-if-unchanged
+   Otherwise no so useful for people to use customize for
+   prover config settings (we'd need to shadow them all again for
+   each assistant for this to work smoothly).
+   Sure sign saving will fail is when you see "this option has
+   been changed outside customization buffer"
+   At the moment even setting config variables in a hook is tricky,
+   because proof-config-done is called before the hook variables for the
+   new mode are.  Our new version of define-derived-mode needs
+   to address this.
+
+X Proofs in Isabelle scripts can be non-interactive.  Non-interactive
+  proofs have only one command, effectively.  It might be useful
+  to find a way to integrate these into Proof General nicely.
+
 X Code in proof.el assumes all characters with top bit set are special
   instructions to Emacs.  This is rather arrogant, and precludes proof
   systems which utilize 8-bit character sets!  Needs repair.  (3h)