Items removed, items added.

1 files changed, 23 insertions, 15 deletions

diff --git a/todo b/todo
index 6931b2a1..c5c991ef 100644
--- a/todo
+++ b/todo
@@ -14,6 +14,26 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
+A* FIX INDENTATION CODE, EDITING .ML (& other?) FILES IS CHRONICALLY SLOW.
+  This is going to hit us hard as soon as the mode gets used in
+  earnest.
+  (da, 2hrs: will investigate if fault lies with Isabelle syntax config)
+  (8hrs, estimated time to fixup indentation code otherwise.  May be
+         best removed altogether, or replaced with elisp code clone)
+
+B ROBUSTness: deal gracefully with possibility that goals buffer is
+  killed during session.
+
+B 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)
+
+B proof-shell-noise-regexp: seems unused at present, but set
+  in the specific directories.  Either use it or be rid of it!
+
 A byte-compilation: continue fixups for clean byte compile.
   Need to compile from clean Emacs to see proper warnings.
   Check that byte compilation (and compiled code!) 
@@ -275,9 +295,6 @@ X Comment support is not very generic: we don't support end-of-line
   terminated comments.  Is there any case where this might be
   worthwhile?  (2h to add it).
 
-X Splash screen: Add fancy text logo to it.  Centre the display
-  prettily.
-
 X Write a Makefile for the distribution.  It can do things like
   install the info file properly.  The work is at the moment done
   in the RPM spec file instead.
@@ -392,16 +409,9 @@ C Improve coqtags. I cannot handle lists e.g., with
 * Here are things to be done to Isabelle Mode
 =============================================
 
-A* Fix bug in undo, maybe related to below?
-
-A* Fix output handling routines to not display parts of messages.
-   Intermittent problems parsing output.  Seems to depend on
-   what has been run before.  E.g. first time starting process
-   might not display goal.  Try to find repeatable case.
+A* Check all regexps are suitable instantiated.
 
-A* Add annotations to prompt and output using Isabelle's ml_prompts.
-
-A* Make theory files go blue.
+A Fixup multiple file handling with theory loader hacks to Isabelle.
 
 D Implement completion for Isabelle using tables generated by
   the running process.
@@ -411,7 +421,7 @@ D Add useful specific commands for Isabelle.  Many could
   (probably a week's work to bring together Isamode and proof.el,
    making some of Isamode generic)
 
-D Add ability to choose logic.  Maybe not necessary: can use default
+X Add ability to choose logic.  Maybe not necessary: can use default
   set in Isabelle settings nowadays, in the premise that most people
   stick to a particular logic?   But then no support for loading
   user-saved databases.
@@ -422,8 +432,6 @@ X Write perl scripts to generate TAGS file for ML and thy files.
 
 X Manage multiple proofs (markers in possibly different buffers)
 	 
-X Add Isabelle logo to splash screen.  (30 mins)
-
 * FSF Emacs
 ===========