[isabelle-dev] error in cook book ?

[Nils Jähnig]

1) so i stay with 2009-2.

>> 3)
>> And finally a question: i can't see messages, like from print_tac or
>> the examples around 1), in emacs. so i used PGeclipse. which option do
>> i have to (un)check, to see those messages in emacs?
>
> According to the sources of Isabelle2009-2, print_tac outputs on the
> "tracing" channel.  It is up to the frontend where that appears visually in
> the end.  Proof General / Emacs version 3.7.x and pre-4.x have a separate
> "*trace*" buffer for that.  It depends on the actual Emacs version, OS
> platform, user preferences etc. how that behaves in detail. You might have
> to switch to that Emacs buffer explicitly.
>
> Did you really manage to run PGEclipse?  I have never seen it in action
> myself.

yes, i found this trace buffer, but it is not really convenient to
work with, as it does not auto clear (i found now C-x C-w and try to
use it) and informations there (especially in the cook book) are meant
to be together with the other output.
and i have an Isabelle-buffer, where all information is displayed (i
think this one is read by PGEclipse).
but using "by simp" displays the informations written with pwriteln
(Pretty.writeln) in the response buffer together. is this something
"by" does?

i suppose "pre-4.x" does not mean "before 4.x" but "4.x-prerelease",
as buffer-behavior is the same with the latest PG.

The PGEclipse is kind of working, but not enough, to work with it. it
has problems with "undo previous proof command", especially if you
have ML-code in the same file.
So at the moment all it does is looking much more user friendly than
emacs, and displaying the output as i want it, but i have to restart
often, so it is not yet an option.

/Nils