Fixed up proof-shell-proof-completed mess nicely.

1 files changed, 14 insertions, 10 deletions

diff --git a/todo b/todo
index a6b1750d..ddbc5e6b 100644
--- a/todo
+++ b/todo
@@ -52,16 +52,6 @@ X (Low)		e.g. probably not worth spending time on
   default way of setting font-lock-keywords, removing from
   proof-easy-config and changing each supported prover instance.
 
-**** A Fixup silly mess introduced by Isabelle's over the top 
-  proof-shell-proof-completed-regexp.  We shouldn't match on
-  the whole output, that was the point of start-goals and end-goals.
-  Instead we should treat the proof-completed as a case within
-  start-goals and end-goals, as well as outside it for other
-  provers.  Then automatically display will be in right place.
-  Shouldn't need proof-goals-display-qed-message any more.
-  This change not yet in 3.1 because it risks changing behaviour
-  of other provers.
-
 **** B Modify response display routine a bit to center around recent output,
   or display top, for long output.    Makes better sense for big 
   screen-fulls, perhaps?  Or maybe display top with an itimer to
@@ -88,6 +78,20 @@ X (Low)		e.g. probably not worth spending time on
 
 ** 2. Things to in the generic interface
 
+*** X Multiple session architecture (difficult)
+
+  With some major re-engineering, PG could be made to work with multiple
+  provers at once, and multiple instances of the same prover.
+
+  Ideas: - introduce "session" notion
+	 - have list of current sessions in progress,
+	   values of active scripting buffer and other per-session vars
+	   for each one
+         - proof shell filter and other functions must automatically
+           switch context to correct session
+         - force everybody to use proof-easy-config macro, and set
+	   <prover>-var automatically from <proof>-var there,
+	   to get defaults for new sessions.
 
 *** C Is there a way to make colours defined for x work in mswindows too?