Hi, why does proof-retract-until-point make the current buffer the active scripting buffer? It seems that Proof General anticipates that the user starts asserting immediately afterward.
However, it might also be the case that the user does only make some very small change and then goes to the previous active scripting buffer (or to some other buffer) and continues processing there. In this case the call to proof-activate-scripting could have been saved. While for most proof assistants the additional call to proof-activate-scripting is probably not noticeable, for Coq it involves killing and restarting the proof assistant. I am posting this because of the following: For Coq (and probably other proof assistants as well) there are a number of small changes that are processed in the following way. While working in A you notice that such a small change is required in B, which is a locked ancestor of A. So you change to B, unlock it, make the small change and _immediately_ go back to A, asserting to the point where you left. Examples for such small changes are: - adding a simple definition - changing an Import into an Export - making an explicit argument implicit or vice versa. In all these cases it is right to completely retract the current scripting buffer A, because this ensures that the changes in B are recompiled and loaded. However, it is not necessary to kill and restart coqtop. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
