Custom Query (361 matches)

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.

Using comment-dwim and kill-rectangle in the locked region triggers several bugs. All the following is done with the read-only option set to "Undo On Edit".

1. uncomment with comment-dwim at the end of the locked region

• in the attached file, assert until line 4, behind the first comment
• put the comment in the locked region into the (emacs) region
• do comment-dwim (M-;)
• asserting again until line 4 gives the error "a already exists"

2. uncomment in the middle of the locked region

• assert all of dwim.v
• put the first comment into the emacs region and do comment-dwim
• this gives a strange error "User interrupt." and leaves *) at the end of the line

3. comment in the middle of the locked region

• open dwim.v and clear the comment on line 3
• assert the complete buffer
• mark line 3 and do comment-dwim
• this gives a strange error "if: Region is read-only" and does not put *) at the end of the line

kill-rectangle (C-x r k) has similar problems as can be seen on the second comment. Maybe comment-dwim uses kill-rectangle internally.

Bye,

Hendrik

open a new file a.v and put just a comment start (* into it. proof-assert-next-command-interactive gives then the error "number-or-marker-p, nil"

Hendrik