Added some items

1 files changed, 9 insertions, 3 deletions

diff --git a/todo b/todo
index f2c9cb6c..87a2f9b0 100644
--- a/todo
+++ b/todo
@@ -33,9 +33,6 @@ C  The semantics of `proof-script-buffer-list' is ambigous. The first
    dynamically if a buffer is instrumented for scripting, contains a
    locked region, etc. (4h, including testing)
 
-
-
-
 A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report (2+2 days; da + tms)
 
@@ -47,6 +44,15 @@ A* FIX INDENTATION CODE, EDITING .ML (& other?) FILES IS CHRONICALLY SLOW.
   (8hrs, estimated time to fixup indentation code otherwise.  May be
          best removed altogether, or replaced with elisp code clone)
 
+C Regions in script buffer have nice "name" property and configurers
+  have to set regexps carefully so that it works, but is it actually
+  used anywhere?   What's it good for?
+
+B Proofs in Isabelle scripts can be non-interactive.  Non-interactive
+  proofs have only one command.  We need to find a way to integrate
+  these into Proof General nicely.  Perhaps things would work
+  fine simply if these match save goal forms?  (da, 1hr)
+
 C ROBUSTness: deal gracefully with possibility that goals buffer is
   killed during session.   (2h)