Updated todo's for isabelle

1 files changed, 11 insertions, 30 deletions

diff --git a/todo b/todo
index 8dc8b60e..2411dd05 100644
--- a/todo
+++ b/todo
@@ -383,35 +383,16 @@ C Improve coqtags. I cannot handle lists e.g., with
 * Here are things to be done to Isabelle Mode
 =============================================
 
-A* Add annotations to prompt and output.
+A* Fix bug in undo, maybe related to below?
 
-B 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* 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.
 
-B CRUCIAL: Do something to manage .thy and .ML files coherently.
-  At the moment loading one into Isabelle will force the
-  processing of the other.  We could ask that users develop
-  proof scripts in another kind of file entirely, or a file
-  with a different name.  But that's an ugly hack.
-  But what else can we do??
-  (Probably answer: Isabelle needs to support non-automatic
-  reading of ML file: a function "use_thy_only" ).
+A* Add annotations to prompt and output using Isabelle's ml_prompts.
 
-B (part of above): Handle proof-retract-file by querying Isabelle
-  about the decendants of a file.  Then all the descendents can
-  also be unlocked.
-
-B (part of above): add multiple file handling for Isabelle
-  (4h).  
-   Work left to do:
-
-     test sending of "retract_file" command to Isabelle.
-     Handle theory files better.
-
-
-X Write perl scripts to generate TAGS file for ML and thy files.
-  (6h, I've completely forgotten perl), or better:
+A* Make theory files go blue.
 
 D Implement completion for Isabelle using tables generated by
   the running process.
@@ -427,11 +408,11 @@ D Add ability to choose logic.  Maybe not necessary: can use default
   user-saved databases.
   (ponder this)
 
-X New features ideas:
-   1. Manage multiple proofs (markers in possibly different buffers)
-	 
-B Set wakeup-char by using Isabelle's ml-prompts function.
+X Write perl scripts to generate TAGS file for ML and thy files.
+  (6h, I've completely forgotten perl), or better:
 
+X Manage multiple proofs (markers in possibly different buffers)
+	 
 X Add Isabelle logo to splash screen.  (30 mins)
 
 * FSF Emacs