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"
   more useful?

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

Reply via email to