Updated

2 files changed, 35 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index df4f2442..3fc2882d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -97,7 +97,7 @@ LEGO Changes
 ------------
 
 * Proofs which have no save command are now closed off automatically
-  when a new goal is begun, mirroring the behaviour of LEGO.
+  when another command arrives, so undo-redo is more flexible.
 
 
 Isabelle and Isar Changes
@@ -109,14 +109,13 @@ Isabelle and Isar Changes
   and saves of the old form val thm = result.
 
 * Proofs which are "unfinished", i.e. have no qed or result,
-  are now closed off automatically when a new goal is begun,
-  mirroring the behaviour of Isabelle.
+  are now closed off automatically, mirroring the behaviour 
+  of Isabelle.  This does not apply to Isar.
 
 * Confusing display of only last error is fixed: multiple
   error messages are now coalesced properly.
 
 
-
 Only in the developers' release
 -------------------------------
 
@@ -136,11 +135,12 @@ Internal changes for developers to note
   The aim is to make it easier to adapt to new proof
   assistants.
 
-* Proofs which are "unfinished", i.e. have no qed or result,
-  are now closed off automatically when a new goal is begun.
-  The new code only applies if proof-nested-goals-allowed is
-  nil (the default).  Setting this variable to t forces 
-  identical behaviour to before.  The default for Coq is t.
+* A new setting proof-completed-proof-behaviour allows for
+  more flexible ways of managing goal...save regions, including
+  automatically closing them when the first command after
+  the proof is completed arrives.  This means we can handle
+  proof assistants which do not have an explicit save command
+  now.   See the documentation of proof-completed-proof-behaviour.
 
 * Renamed some configuration variables for uniformity:
     proof-ctxt-string -> proof-context-command
diff --git a/todo b/todo
index 3daeb68d..f7ae10d8 100644
--- a/todo
+++ b/todo
@@ -82,10 +82,21 @@ B SMALL DELTAS:
   - Difference in menubar appearance depending on whether X-Symbol
   is loaded before Proof General or not.
 
-
 B Have seen "confused" bug: shows up when do lots of C-c C-n as
   process is starting up.
 
+B Making undoing better.
+  Rather than calculating an undo command each time an undo command
+  is needed, another idea would be to keep the undo command in the
+  span.  Then when we amalgamate spans we can construct new undo
+  commands.  When we come to issue an undo, we either need to do
+  each undo step in turn in reverse, just the final one, or perhaps
+  some proof-assistant dependent filtering/modification of the
+  set.   At the moment, though, PG is rather keen on issuing just
+  one command to forget to some specific place in the script.
+  [Maybe a design principle is that spans should coincide with
+   undoable regions]
+
 D Why don't PG's minor modes appear on XEmacs minor mode menu?
   (C-right on status bar)
 
@@ -755,6 +766,20 @@ C Inoking an "Expand" command produces a new proof state. But this is
   ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
   definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)
 
+C Even with the more flexible region model, with 
+  proof-nested-goals-behaviour=closequick, Proof General doesn't
+  do quite the right thing.  Forget for a definition when inside
+  a proofstate kills off the whole proofstate.  Effectively,
+  the definition is *global* rather than local to the proofstate,
+  and could perhaps be lifted to before the goal
+  (with the lift-global nonsense not so daft after all?  Editing
+   behind the user's back is still objectionable though).
+
+  Another alternative fix would be to trigger some retraction action
+  on seeing the "Abort" regexp, rather than assuming it is the result of
+  some retraction action.  More generally this could be used for error
+  handling.
+
 C fix Pbp implementation (10h)
 
 D Improve legotags. It cannot handle lists e.g., with