Added two new todos

1 files changed, 14 insertions, 0 deletions

diff --git a/todo b/todo
index 97f04be4..87f835ce 100644
--- a/todo
+++ b/todo
@@ -40,6 +40,14 @@ A* multiple files bug fix:
    --> One case now fixed by allowing current scripting buffer to
     be retracted.  Are there other cases?  (da to investigate)
 
+C  Strange behaviour when killing and re-visiting files that
+   haven't been completely processed.  Since they stay on
+   the proof-included-files-list, on re-visiting, they are
+   marked atomic as completely processed!  
+   Possible fix:  if file hasn't been completely processed, 
+   maybe retract (and hence remove from proof-included-files-list),
+   or query the user?
+
 C  The semantics of `proof-script-buffer-list' is ambigous. The first
    element is the current script buffer, we are not quite sure what
    role the other elements ought to have. We propose to abandon
@@ -443,6 +451,12 @@ A Fixup multiple file handling with theory loader hacks to Isabelle.
 
 C derive an isa-response-mode from proof-response-mode; see lego.el (10min) 
 
+C Obscure process-handling problem which prevents goal appearing
+  when Isabelle HOL is started.  Visit example.ML, do "next command".
+  Suggested process: debug proof-shell-filter.  Has something to
+  do with annotated prompts.
+  (4h)
+
 D Implement completion for Isabelle using tables generated by
   the running process.