From 80865dca3f242338eb3c4fa001d02a35a554c884 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 14 Nov 1999 10:14:13 +0000 Subject: Updated --- CHANGES | 18 +++++++++--------- todo | 27 ++++++++++++++++++++++++++- 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 -- cgit v1.2.3