assert newly added text in ancestor fails

[coquser]

See the test case in coq/ex/test-cases/change-ancestor/README.

The problem appears when one asserts text that has just been added at the end of an completely locked ancestor. Then Proof General sends only the newly added portion to Coq instead of the complete buffer.

[coquser]

The problem is obviously that proof-activate-scripting is called after proof-segment-up-to. However, the bug is still present after moving the call to proof-activate-scripting before proof-segment-up-to.

[coquser]

patch

[coquser]

Actually, moving proof-activate-scripting before proof-segment-up-to does fix the problem, see the attached patch.

With that patch proof-assert-until-point-interactive behaves as expected.

However, proof-assert-next-command-interactive behaves a bit strangely: When used to assert the first command of the text that was appended to the ancestor, it asserts everything up to the point before that first command. The reason is that proof-assert-next-command-interactive moves point to the end of the locked region. In such a case proof-assert-until-point would normally just assert the next command. However, with the patch, the ancestor is unlocked at the start of proof-assert-until-point and therefore proof-assert-until-point only asserts until point, which is the end of the locked region before calling proof-assert-next-command-interactive.

I would leave this proof-assert-next-command-interactive anomaly as is: For Coq it is not precisely clear what the next command of a locked ancestor with newly added text should be. And just typing C-c C-n again will assert the newly added command.

[David Aspinall]

OK, I've taken a look at this now and tried out the patch in Isabelle, where I don't think it will do harm. I agree with your suggestion -- there are a few odd pointer/region movement variations like this that are hard to get to be completely consistent. I think people adjust quickly to the behaviour that actually happens.

Patch committed now.