David Aspinall <david.aspin...@ed.ac.uk> writes:
> 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? ]
Yes, if B is visible in some window then its point is not
> 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"
I am going to try that.
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
Yes, I though about this too. However, there should be a
threshold, such that the mark is only set if point moves more
than threshold lines. Otherwise simple one-line undo commands
will clutter the mark ring.
ProofGeneral-devel mailing list