Discussion:
let proof-retract-buffer only move point when called interactively
Hendrik Tews
2012-05-31 14:48:11 UTC
Permalink
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

Loading...