> 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 there a difference between what happens with B invisible and visible? ]
> 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.
I agree that's not useful for your suggested use case, although it certainly
matches the understanding of "follow the locked region". Do you find "follow
the locked region down" more useful?
As an improvement we might set the mark so the user could simply hit C-u
C-space to jump back, then C-RET to carry on scripting.
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.