Isabelle: trying to undo a step fails for me

[RafalKolanski]

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.

[RafalKolanski]

Actually, nevermind, turns out our version of Isabelle doesn't have "linear_undo" so no wonder it doesn't work. Should get fixed when we upgrade.

[RafalKolanski]

Furthermore, thank you for the option to turn linear_undo off that I just discovered (isar-use-linear-undo). I turned it off and undo works again.