Added some items after user feedback. Also some *** probs.

1 files changed, 20 insertions, 11 deletions

diff --git a/todo b/todo
index 3a426eec..bc3814c8 100644
--- a/todo
+++ b/todo
@@ -24,9 +24,21 @@ A***  Documentation polishing.
 A***  BUG: FSF Emacs process handling (check on proof-shell-insert fix), 
       killing buffer problems.
 
-A***  BUG: FSF Emacs and LEGO term markup: aref out of range.
+A***  outline mode when proof-strict-read-only is nil, does it really
+work?
 
-A ish Fixup LEGO output.
+A*** QUESTION: why do we have proof-shell-proof-completed-regexp's
+perhaps objectionable behaviour of forcing the response buffer?
+Would it be safe just to set the proof-shell-proof-completed flag
+and output as usual?   (The effect would be to allow Isabelle's
+completed proof message to appear in the goals buffer since it's
+marked up as a proof state output)
+
+A*** Possible bug [Isabelle/all]:
+ at the top of a script buffer, sometimes special commands like
+ ProofGeneral.kill_goal(); are inserted without reason
+
+A ish Improve LEGO output.
 
 A ish BUG: catch bug on Solaris when process shell killed.
 
@@ -279,6 +291,9 @@ D Display management is much better than it was, but perhaps
     Perhaps retraction should set the flag to ensure
     it's cleared.
 
+X Consider filtering out special annotations from shell buffer
+  rather than merely making them invisible.
+
 X Add ChangeLog to developers distribution to give them
   something more to look at.  (30mins).
 
@@ -489,24 +504,18 @@ X Sections and files are handled incorrectly.
 * Here are things to be done to Isabelle Mode
 =============================================
 
-A Fixup multiple file handling with theory loader hacks to Isabelle.
+A auto-adjust Pretty.setmargin when window is resized
 
 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.
 
 D Add useful specific commands for Isabelle.  Many could
   be added.  Would be better to merge in Isamode's menus.
-  (probably a month's work to bring together Isamode and proof.el,
-   making some of Isamode generic)
+  (however, probably a month's work to bring together Isamode 
+   and proof.el, making some of Isamode generic)
 
 X Add ability to choose logic.  Maybe not necessary: can use default
   set in Isabelle settings nowadays, in the premise that most people