Custom Query (361 matches)
Results (43 - 45 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #390 | duplicate | Odd progress markers in text mode | ||
| Description |
Mac OS X Snow Leopard. Running with /usr/bin/emacs in text mode produces strange progress markers within the actual text: =>eory Scratch imports Main begin term x theory Scratch imports Main begin =>rm x |
|||
| #427 | duplicate | defpacustom and undo | ||
| Description |
Hi, defpacustom settings are not preserved over undo, at least not for Coq. Consider, for instance, switching "Print fully explicit" on in the middle of some file, then after undo, you get again normal printing behavior. (For Coq, this is of course not really surprising.) I don't know, if we really want to implement settings that are preserved over undo. However, it would be nice, if the defpacustom variable is reset to normal state (and thereby also its menu entry), if its effect is lost because of an undo. Hendrik |
|||
| #433 | duplicate | unexpected cursor position after stepping through command with terminator at line ending | ||
| Description |
Disclaimer: I am fairly new with PG and not yet used to the terminology, so feel free to correct me when I use the wrong terms.
My setup: Issue: When I am stepping interactively through a coq script with either the next-command instruction or with the activated electric terminator and the terminator (i.e. the dot) happens to be the last character of that line in the script file, the editor cursor jumps to the beginning of the following line. However, what I would expect is that the cursor either remains where it is or at least that it is positioned after the terminator but on the same line. This doesn't make a huge difference when stepping through an existing script but when one is developing a new script this behaviour can become really irritating, e.g. with the electric terminator I'd practically be forced to either write each command on a new line or constantly press the back key to reposition the cursor to where I want it. In case that the former behaviour is intentional, a switch to change the behaviour might be useful (feel free to point me in the right direction if something like this already exists, I couldn't find it so far). Otherwise adjusting this could be considered usability enhancement. |
|||
