comment-dwim and kill-rectangle in the locked region

[coquser]

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

[David Aspinall]

Hmm, nasty stuff! What's happening is that those deletion commands impose a temporary narrowing on the buffer which confuses the automatic retraction into undoing the wrong part of the buffer.

I've added a patch to remove the restriction during the automatic retraction, but I'm not sure if it fully solves the problem. Could you check (CVS head has patch in proof-script.el)?

[coquser]

Replying to da:

There is an improvement in that Proof General issues now the right backtrack command and the prover session stays consistent.

However, kill-rectangle and comment-dwim do not behave correctly, when used in the locked region:

• fully assert the attached dwim.v
• make a region from line 5 to 9 (around the second comment)
• do comment-dwim then

The result is then

Definition c :=

• a + 2. *)

where the correct result would be

Definition c :=

a + 2.

Hendrik

[coquser]

It would be nice if there were a button NO WIKI FORMATTING.

The second have of my reply should have been

The result is then

    Definition c := 
     *   a + 2.
     *)

where the correct result would be 

    Definition c := 
      a + 2.

[David Aspinall]

Fixed, I hope.

Thanks for pointing that out -- the retraction function needed to wait for retraction to complete before returning, otherwise it could cause a read-only error part way through the calling function.

[coquser]

This is great! Thanks a lot for the fix!!

Hendrik