Custom Query (361 matches)
Results (43 - 45 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #131 | fixed | Add preference setting for interrupt command | ||
| Description |
This is prover specific and (in the case of Isabelle), unfortunately hard to determine. Code currently has "killall -2 HOL" hardwired. This should be moved to a prover preference setting (near Use PGIP interrupts) |
|||
| #137 | fixed | Add output highlighting/insert support for Isar and sledgehammer ("Sendback") | ||
| #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. |
|||
