Split low-level todo into several files.

1 files changed, 59 insertions, 0 deletions

diff --git a/isa/todo b/isa/todo
new file mode 100644
index 00000000..b5b4ad04
--- /dev/null
+++ b/isa/todo
@@ -0,0 +1,59 @@
+-*- mode:outline -*-
+
+* See also ../todo for generic things to do, priority codes.
+
+* Things to do for Isabelle
+===========================
+
+B auto-adjust Pretty.setmargin when window is resized.  Use
+  generic code once it's implemented.
+
+D Implement completion for Isabelle using tables generated by
+  the running process.  Ideally context sensitive.
+  Would be a nice addition. (1 week)
+
+D Add useful specific commands for Isabelle.  Many could
+  be added.  Would be better to merge in Isamode's menus.
+  (however, probably 2 week's work to bring together Isamode 
+   and proof.el, making some of Isamode generic)
+
+D Switching to other file with C-c C-o could be more savy
+  with file names and extensions (use some standard function?)
+
+X weird bug: interrupting Isabelle process (under sml-nj) sometimes
+  doesn't return, why? (see first half of interrupt error only:
+
+    *** Interrupt.
+    *** At command "time_use".
+  
+    uncaught exception ERROR
+      raised at: library.ML:1100.35-1100.40
+  But not "uncaught exception" part.  
+  What is worse: prompt disappears!  But process still seems to be
+  there underneath.  Not sure where this bug comes from.
+
+  Moreover, killing process then hangs Emacs with message 
+  "cleaning up", and get error
+    (1) (error/warning) Error in process sentinel: (no-catch exited t)
+
+  To see if this is some SML/NJ or Isabelle weirdness, test in 
+  xterm: use "ROOT.ML", interrrupt, use "ROOT.ML" again.
+  sig 11!  (flaky hardware?)  
+    /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2ad09c43
+  Not reliably repeatable, but:
+    ProofGeneral.isa_restart(); 
+    /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b
+
+X Add ability to choose logic.  Maybe not necessary: can use default
+  set in Isabelle settings nowadays, in the premise that most people
+  stick to a particular logic?   But then no support for loading
+  user-saved databases.  (ponder this)
+
+X Write perl scripts to generate TAGS file for ML and thy files.
+  (6h, I've completely forgotten perl).  
+
+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!
+
+