Hi,
why does proof-retract-until-point make the current buffer the
active scripting buffer? It seems that Proof General anticipates
that the user starts asserting immediately afterward.
However, it might also be the case that the user does only make
some very small change and then goes to the pre
Hi,
in its default setting (which is locked) proof-follow-mode
ensures that point is at the end of the locked region. Consider
the following case: The user switches to buffer A, which is a
locked ancestor of the current scripting buffer B. In order to do
some changes in A the user unlocks A, there
> why does proof-retract-until-point make the current buffer the
> active scripting buffer? It seems that Proof General anticipates
> that the user starts asserting immediately afterward.
Not particularly, this is to enforce the simplifying invariant that there is at
most only one buffer which ca
> 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
