Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:


Results (28 - 30 of 361)

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
Ticket Resolution Summary Owner Reporter
#304 invalid Isabelle: trying to undo a step fails for me David Aspinall RafalKolanski
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 David Aspinall RafalKolanski
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

apply (moo)

Isabelle version: 2009-1

PG version: latest CVS as of right now.

#6 fixed Add code folding for proof scripts David Aspinall anonymous
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.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
Note: See TracQuery for help on using queries.