Custom Query (361 matches)

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

if i close an active editor, the GotoAction? throws an NPE when trying to undo-all the proof script. thereafter the user cannot activate any script (even re-opening the same file) until the prover is restarted.

see comments in PGRetargetableAction.setBusy(): it looks like this call does not do what it is supposed to if the document is set manually (as it is from ActivateAction?.closeDownScript).

as a larger issue, we need to consider the different cases of closing (and re-opening) a script:

(a) if the script is fully processed, the user probably wants to keep it in the prover's memory (i.e. don't retract); however they do need a way to retract it later, probably re-opening the script should "remember" it is fully processed. (not sure what we do currently)

(b) if the script is partially processed, it is probably okay to undo all (which we currently do, modulo fixing the above bug). however it would be nicer, i think, to give the user the option to (a) discard (undo all); (b) finish processing; (c) cancel. (and maybe option to "do nothing", leave partially processed, and restoring it if they open the file later.) we used to do this, but it is commented out (in ActivateAction?). possibly because we were not getting reliably informed about shutdown events and so were pointlessly prompting the user on shutdown...)

I seem to be able to enable the electric-terminator using a hook in my .emacs file (although it doesn't work right -- see issue 371), but "C-c ;" gives me "C-c ; is undefined".