Opened 9 years ago

Closed 9 years ago

Last modified 9 years ago

#403 closed defect (fixed)

comment-dwim and kill-rectangle in the locked region

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

Description

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"
  1. 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
  1. 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

Attachments (1)

dwim.v (114 bytes) - added by coquser 9 years ago.

Download all attachments as: .zip

Change History (6)

Changed 9 years ago by coquser

Attachment: dwim.v added

comment:1 Changed 9 years ago by David Aspinall

Status: newaccepted

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)?

comment:2 in reply to:  1 ; Changed 9 years ago by 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

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

comment:4 Changed 9 years ago by David Aspinall

Resolution: fixed
Status: acceptedclosed

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.

comment:5 Changed 9 years ago by coquser

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

Hendrik

Note: See TracTickets for help on using tickets.