Made desired usability changes more explicit and detailed.

Mentioned output formatting spurious newlines issue for Isabelle.

1 files changed, 32 insertions, 7 deletions

diff --git a/todo b/todo
index 8a2bc840..82e30d38 100644
--- a/todo
+++ b/todo
@@ -37,14 +37,35 @@ X (Low)     probably not worth spending time on
 * Things to in the generic interface
 ====================================
 
-A Usability enhancements:
-   1. Movement of point after assert/retract commands
+A Usability enhancement:
+   Movement of point after assert/retract commands
         - configure by default for one command/line.
 	- Add option for many commands per line.
 	- Maybe shell like behaviour with pressing return?
-   2. Optional argument to delete region removed from C-c C-u
-   3. Extra toolbar and menu commands
-	- Toolbar button to display current proof state
+
+A Usability enhancement:
+   Optional argument to delete region should be removed 
+   from C-c C-u, pressing quickly in succession can delete
+   from buffer
+
+A Usability enhancement:
+   Rationalize next and undo.  Make same as toolbar 
+   commands and have different commands for power users
+   to assert/retract until point.
+
+A Usability enhancement:
+   Have toolbar button/command to goto a point.
+   Proof General itself should work out whether it's a 
+   retraction or advancement!
+
+A Usability enhancement:
+   Add toolbar button for interrupting.
+
+B New feature:
+   Add command and button for searching for a theorem
+   (possibly matching a given constant, or the proof state).
+
+B Finish design of new icons.  
 
 D bug: outline mode when proof-strict-read-only is nil ought to
   work, but there may be problems.
@@ -592,15 +613,19 @@ A Multiple files needs careful testing.  There are cases when
 
 B auto-adjust Pretty.setmargin when window is resized
 
+C Unify display of proof output for final level "No subgoals" 
+  case with other levels  (i.e. remove spurious newlines).
+  NB: spurious newlines may be liked by other provers.
+
 C derive an isa-response-mode from proof-response-mode;
   see lego.el (10min) 
 
 D Implement completion for Isabelle using tables generated by
-  the running process.
+  the running process.  Would be a nice addition. (4 hours)
 
 D Add useful specific commands for Isabelle.  Many could
   be added.  Would be better to merge in Isamode's menus.
-  (however, probably a month's work to bring together Isamode 
+  (however, probably two 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