Custom Query (361 matches)
Results (28 - 30 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#304 | invalid | Isabelle: trying to undo a step fails for me | ||
Description |
I am uncertain if my version of Isabelle is to blame (i.e. not *exactly* 2009, but close), but with the latest CVS sources I am unable to undo a step, e.g. theory Pointers imports Main begin text {* blah *} typedecl virtual I advance a step forward, everything is fine, next step, fine. Try to go a step back to change "blah" for instance, and I get: *** Outer syntax error: command expected, *** but identifier linear_undo was found and the new underline thing kicks in on that statement. Issue occurs with Emacs 23.1.1. I don't know if I'm alone in this. |
|||
#322 | invalid | Isabelle: "error in process filter: Wrong number of arguments" when using tracing() in ML | ||
Description |
When using the tracing function in an ML block, Proof General generates the error attached in SC.txt To reproduce this error, use the attached SC.thy. It occurs at
Isabelle version: 2009-1 PG version: latest CVS as of right now. |
|||
#6 | fixed | Add code folding for proof scripts | ||
Description |
Add code folding for proof scripts. Hua Yang had some experimental code which hard-coded Isabelle syntax; this should be revisited and revised to use the document parse instead. |