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 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
