Custom Query (361 matches)
Results (25 - 27 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #187 | fixed | If sent command fails, don't move the cursor. | ||
| Description |
Typical work flow is: change something, send using c-c c-return. If the command fails, it's probably due to the something I just changed, where I had the cursor in the first place. Unfortunately, proof general moves it to the end of the current command, making me have to go back manually, change things again, etc. Being able to keep the cursor where it is if the command fails would be really nice. |
|||
| #188 | fixed | Option to treat comments as individual statements. | ||
| Description |
The commands of type (* comment *) and -- "comment" are absorbed as part of the previous command. They hardly ever describe the previous command, instead describing the *following* one. I would much prefer if when I pressed "previous" or performed an undo using c-c c-return, I could go up to before the comment without undoing the previous command. This is one of the reasons I've taken to working with strict read-only turned off, but for beginners this is not such a good idea. |
|||
| #258 | fixed | Copying from response buffer also copies colour control chars | ||
| Description |
In the latest CVS (updated Oct 28th, but problem existed previously): If I copy something colourful from the response buffer, like say a green "xs", when I paste it into the proof (text) buffer, I'll get something like AFxsAA. Copying subgoals out of the response buffer and proving them as separate (generalised) lemmas is a common use-case for me. I'm using Isabelle/HOL. |
|||
