Opened 17 years ago
Closed 13 years ago
#138 closed defect (fixed)
Can't insert text after locking a comment
Reported by: | Evgeny Makarov | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.2 |
Component: | 2:pg-emacs | Keywords: | insert after comment |
Cc: | emakarov@… |
Description
Dear Proof General developers,
When I issue the proof-assert-next-command-interactive (C-c C-n) command over a comment in a Coq file, the comment is joined to the locked region and the cursor is positioned at the end of the comment. After that, I cannot insert any text: whatever I type, I get a beep and a message "Region is read-only" in the minibuffer. As far as I noticed, this only happens when I type just after I have locked a comment; after I process other Coq commands, I am able to enter text.
This happens when I am using the CVS snapshot 3.7pre070704 even with no .emacs file.
By the way, when I was writing this, the link "bug tracker" on the PG home page http://proofgeneral.inf.ed.ac.uk/ was broken.
Change History (5)
comment:1 Changed 17 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
comment:2 Changed 13 years ago by
Resolution: | fixed |
---|---|
Status: | closed → reopened |
I am still having the same issue in PG 4.1 (the latest CVS version) and Gnu Emacs 23.2.1. After C-c C-n, the cursor is put on the line after the comment, but if I put it right after *), I can't insert anything and get the message "Region is read-only". Interestingly, I can insert text inside the comment even though it is locked (I suppose this is correct).
comment:3 Changed 13 years ago by
Cc: | emakarov@… added |
---|
comment:4 Changed 13 years ago by
Milestone: | PG-Emacs-3.7 → PG-Emacs-4.2 |
---|
Confirmed, thanks for the report and apologies for the regression.
Will need a bit more investigation to fix but debugger shows same underlying fault as before: the empty queue span is left in the buffer at the point just after the comment. The changed logic in proof-add-to-queue
may be to blame.
comment:5 Changed 13 years ago by
Resolution: | → fixed |
---|---|
Status: | reopened → closed |
Fixed now in version 12.2 of proof-shell.el (CVS head, today's pre-release).
Fixed in proof-shell.el 8.28 (queue span wasn't detached in this case). Many thanks for the report.