Custom Query (361 matches)
Results (67 - 69 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#164 | wontfix | Error with GNU Emacs 21.4.1/C-c C-BS | ||
Description |
I'm going through the "walkthrough example in Isabelle/Isar?" in section 2.1 of the user manual. When I come to the bit about backing up with C-c C-BS, emacs gives the error "wrong type argument: listp, #<overlay from 74 to 92 in Walkthrough.thy>". The same happens if I choose Undo Step or Delete Step from the menu. Playing around further, if I get to the line "then obtain B and A .." and then press C-c C-RET, I get a similar error "error in process filter: Wrong type argument: listp #<overlay..>". After this, if I try to choose "Restart Scripting" from the menu, emacs hangs. I tried this with both ProofGeneral 3.6 and 3.7 and Isabelle2005 under emacs 21.4.1. Any help would be greatly appreciated. |
|||
#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. |
|||
#166 | fixed | Out of sync on illegal escape character | ||
Description |
PG-Emacs: 3.7pre071112 Isabelle: 2007 Here is a reproducible way to get ProofGeneral 3.7pre071112 out of sync with the isabelle2007 process, simply process this theory: theory Scratch imports Main begin
end This happens quite often if you insert latex in your formal comment and forget to convert "..." to {*...*} syntax. Having to restart Isabelle each time is annoying for large theories. |