David Aspinall david.aspin...@ed.ac.uk writes:
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.
Not particularly, this is to enforce the
David Aspinall david.aspin...@ed.ac.uk writes:
In order to do some changes in A the user unlocks A, thereby
retracting B. If B is not visible, then the point in B will
be moved to the beginning of the buffer.
[ is there a difference between what happens with B invisible
and
