I still don't like the fact that Proof General moves point to the
beginning of the buffer, when the buffer is automatically
retracted, because I change the current scripting buffer. See
also the old discussion at
I have now committed a simple fix: proof-retract-buffer only
moves point when called interactively. To distinguish interactive
calls I use the trick described in
section "21.4 Distinguish Interactive Calls" in the Elisp manual.
I am prepared to retract this change and search for a different
solution, if people don't like this change. Note however, that
there are also other cases where point does not follow the locked
region (when proof-follow-mode = 'locked). For instance when
locking or unlocking ancestors, point does not move.
ProofGeneral-devel mailing list