Updated.

1 files changed, 9 insertions, 3 deletions

diff --git a/isar/todo b/isar/todo
index 0adc6508..e6d3ed1d 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,12 @@
 
 See also ../todo for generic things to do, priority codes.
 
+** B Isabelle support for ML and legacy files: would like to remove "isa" instance
+     Could we handle theory files and even allow scripting in ML files
+     at the same time as Isar?  Maybe not, if this is even beyond what
+     Isar interface would allow (unless we send an ML file
+     line-by-line with ML_command?)
+
 ** B theorem dependencies: using Isar's "thm" command does not
    work at top level.  This is annoying for browsing the fully
    qualified dependency names.  (Even the ML_command "thm"
@@ -12,12 +18,12 @@ See also ../todo for generic things to do, priority codes.
 
 ** B visualise dependencies: sometimes not applicable.
 
-** C func-menu: observe proof-syntactic-context (general problem of
-func-menu setup?);
+** C func-menu: 
+	observe proof-syntactic-context (general problem of func-menu setup?);
 
 ** C undo 'use' command: unlock corresponding ML file;
 
 ** 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);
+     Isabelle's pretty-printing subsystem);