Custom Query (361 matches)
Results (25 - 27 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #138 | fixed | Can't insert text after locking a comment | ||
| 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. |
|||
| #153 | fixed | is "proof state" view needed anymore? | ||
| Description |
the CurrentStateView? ("Proof State") doesn't seem to be useful -- only shows "proofstate" pgip messages, which don't seem to come back any more. remove this view so as not to confuse users? (LatestOutputView? is much better.) otherwise improve documentation (and use) of State view so that its purpose clear. |
|||
| #155 | fixed | sending past end doesn't work quite right ("undo" fails, maybe more) | ||
| Description |
if i parse a theory passed the "end" point, "undo" no longer works; ("undo all" sometimes does, but "undo" should give an error at least) i'm also not sure it correctly registers that the theory is closed, when i switch to another theory it wouldn't let me activate it (but that could be do to a failed retract...) |
|||
