David Aspinall <[email protected]> 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
