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
changed.

   > 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
   scripting.

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.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to