in its default setting (which is locked) proof-follow-mode
ensures that point is at the end of the locked region. Consider
the following case: The user switches to buffer A, which is a
locked ancestor of the current scripting buffer B. 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 this behavior really intended? The beginning of the buffer is
not a very useful position. If the user ever switches back to B,
he probably wants to continue at the position where he left.
ProofGeneral-devel mailing list