tuned todo stuff;

2 files changed, 30 insertions, 5 deletions

diff --git a/isa/todo b/isa/todo
index eaad888b..405b209b 100644
--- a/isa/todo
+++ b/isa/todo
@@ -63,10 +63,8 @@ See also ../todo for generic things to do, priority codes.
   user-saved databases.  (ponder this)
 
 ** X Write perl scripts to generate TAGS file for ML and thy files.
-  (6h, any volunteers?).  
+  (60h, any volunteers?) (hard);
 
 ** X Manage multiple proofs, perhaps by automatically inserting
   push_proof() and pop_proof() commands into the proof script.
-  But would lead to unholy mess for script management!
-
-
+  But would lead to unholy mess for script management! (hard!)
diff --git a/isar/todo b/isar/todo
index e7c51108..37f1d500 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,7 +4,34 @@
 
 See also ../todo for generic things to do, priority codes.
 
-** C Combine with isa/ to get single Isabelle PG instance, somehow?
+** B switch to ProofGeneral.undo (after Isabelle99-1 is out!);
+
+** C fix '{{' and '}}' keywords (e.g. proper font-lock, indentation);
+unfortunately the present word boundary regexp does not work since { }
+are already part of comment syntax;
+
+** C undo 'use' command: unlock corresponding ML file;
+
+** C interactive support for diagnostic commands: easy way to run
+thm/prop/term/typ on region in an ad-hoc fashion;
+
+** C provide template for empty theory (or even just for Scratch.thy);
+
+** C proper proof-by-pointing support (hard; needs major reworking of
+Isabelle's pretty-printing subsystem);
+
+** C speedup indentation (rather do this at generic level?); would be
+nice if current indentation stack would be somehow stored within the
+extend(s) processed last;
+
+** C eliminate explicit ";" terminator; rather refer to regexp (note:
+requires {{ }} to be fixed; ideally, current set of keywords would be
+retrieved from the running process, in order to gain robustness);
+
+** C tune behaviour of goals/response buffers (e.g. hide empty
+response buffers when using 2 buffer model);
+
+** D Combine with isa/ to get single Isabelle PG instance, somehow?
 
 Then users could use both proof languages.