Added some suggestions from Markus Wenzel

1 files changed, 49 insertions, 13 deletions

diff --git a/todo b/todo
index ac4f236a..60a9a6e1 100644
--- a/todo
+++ b/todo
@@ -25,6 +25,12 @@ A* multiple files bug fix:
    --> One case now fixed by allowing current scripting buffer to
     be retracted.  Are there other cases?  (da to investigate)
 
+
+    TODO:
+
+     example.thy -> process it -> Doesn't get locked.
+     
+
 A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report (2+2 days; da + tms)
 
@@ -32,30 +38,64 @@ A Check that byte compilation (and compiled code!)
   works for both varieties of Emacs. 
   Fill out Makefile.dist (2hr da)
 
+A* Fixup for non-script buffer locking:
+
+    proof-locked-end called from wrong buffer when error message
+    is output.
+
+    proof-restart-script is now broken (2h 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)
 
-A* Fixup for non-script buffer locking:
+A* Is it possible to let C-c C-c (SIGINT) issue additional process input?
+   Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or
+   rather fail gracefully.
 
-    proof-locked-end called from wrong buffer when error message
-    is output.
 
-    proof-restart-script is now broken (2h da)
+B outline configuration should be generic  (or else documented for
+  each prover separately, since not guaranteed to work for all).
+
 
 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)
 
-B da: goal-hyp: this should be more generic.  At the moment, there are
+C da: Suggested improvement to interface for included files:
+  Currently have two cases: processing a single file, and
+  retracting which updates the included file list arbitrarily
+  (but assumes that only removals are made).  A simpler and
+  more general interface would be to just have the second
+  case, and automatically find removed files and added files
+  between two versions of proof-included-files-list and
+  unlock or lock buffers appropriately.  We could provide
+  a useful default function based on three regexps:
+  retract-file-regexp, add-file-regexp, clear-filelist-regexp.
+  Master regexp process-file-regexp would match all of
+  these cases.   Could be multiple matches of the three above
+  within a single process-file-regexp to avoid processing
+  lots of urgent messages.  (3h)
+
+C da: goal-hyp: this should be more generic.  At the moment, there are
   generic variables which are only used in the specific code:
   proof-shell-goal-regexp and proof-shell-assumption-regexp.
   This is confusing.  I suggest making lego-goal-hyp the
   default behaviour for proof-goal-hyp-fn a hook function.
   That will work for Isabelle too.   (15 mins)
 
+C Output filtering has some buglets:
+   1. proof-shell-filter could miss output in the unfortunate
+      circumstance that a prompt consists of more than one character and
+      is split between output chunks.  Really the matching should be
+      based on the buffer contents rather than the string just
+      received. [IMPORTANT]
+   2. Handling mixtures of urgent and non-urgent messages:
+      at the moment any non-urgent output *before* an urgent
+      message will not be displayed in the response buffer.  [MINOR]
+
 C  proof-goal-command-regexp: add this setting to coq.el.
    Rationalize use of proof-goal-command-p
    (probably can be scrapped now).  
@@ -68,14 +108,6 @@ C  Strange behaviour when killing and re-visiting files that
    maybe retract (and hence remove from proof-included-files-list),
    or query the user?
 
-C  The semantics of `proof-script-buffer-list' is ambigous. The first
-   element is the current script buffer, we are not quite sure what
-   role the other elements ought to have. We propose to abandon
-   `proof-script-buffer-list' and only keep a record of the current
-   proof script buffer in `proof-script-buffer'. We can easily check
-   dynamically if a buffer is instrumented for scripting, contains a
-   locked region, etc. (4h, including testing)
-
 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).
@@ -232,6 +264,10 @@ D Allow bib-cite style clicking on Load/Import commands to go to file.
 D Remove duplication of variables e.g., proof-prog-name and
   lego-prog-name for Coq and Lego. (1h)
 
+X Images for splash screen: could add xpm files for logos 
+  so that XEmacs displays transparent parts properly.
+  (Probably not worth effort of distributing more files).
+
 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