Custom Query (361 matches)
Results (70 - 72 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#209 | fixed | Cursor not visible in *response* buffer (GNU Emacs 22 + Carbon Emacs) | ||
Description |
In the *response* buffer the cursor is not visible, but can be moved as expected. |
|||
#165 | wontfix | Cygwin: font-lock crashes on XEmacs 21.4.20 | ||
Description |
Certain complex response from the prover (Isabelle2007) can make font-lock crash when processing the output for display in *response* buffer. The included file "bad.output" has been fetched from the *isabelle* buffer in the critical situation. It can be replayed by starting a fresh Isabelle2007 / Proof General session on Cygwin and issuing the following Isar command:
This will result in tons of messages like this: (1) (error/warning) Error in process filter: (args-out-of-range *response* 330313 345908) (2) (error/warning) Error in process filter: (args-out-of-range *response* 314717 330312) (3) (error/warning) Error in process filter: (args-out-of-range *response* 299121 314716) (4) (error/warning) Error in process filter: (args-out-of-range *response* 283525 299120) The problem seems to be specific to Cygwin or the particular XEmacs 21.4.20 installation of that distribution. It works fine on various Linux installations of with XEmacs 21.4.21/22. |
|||
#486 | fixed | Disable long indention under quantifiers? | ||
Description |
At some point (I think related to emacs 24) Proof General changed its way for indenting lines under quantifiers. E.g. Lemma foo_bar_baz : forall x y z,
Is there a way to revert to the previous 2-space indent from the indent at the beginning of the line? |