Opened 9 years ago

Closed 9 years ago

#400 closed defect (fixed)

assert newly added text in ancestor fails

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

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.

Attachments (1)

change-ancestor-patch (1.3 KB) - added by coquser 9 years ago.
patch

Download all attachments as: .zip

Change History (4)

comment:1 Changed 9 years ago by 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.

Changed 9 years ago by coquser

Attachment: change-ancestor-patch added

patch

comment:2 Changed 9 years ago by 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.

comment:3 Changed 9 years ago by David Aspinall

Resolution: fixed
Status: newclosed

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.

Note: See TracTickets for help on using tickets.