Custom Query (361 matches)

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

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

The customization groups for Proof General need a bit of tidying: for example, the Proof General Internals group and Prover Config group has settings which appear as CHANGED or UNINITIALIZED.

These probably don't cause any problems in everyday use but are odd to users who browse Customize options.