Hendrik Tews
2012-05-31 14:48:11 UTC
Hi,
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
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html
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.
Bye,
Hendrik
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
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html
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.
Bye,
Hendrik