On Wed, 8 Sep 2010, Nils Jähnig wrote:
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).
I think Christian even had a strong inclination towards tracing output in
some versions of the Cookbook, because it produced a certain wanted
behaviour on a certain version of Proof General / Emacs.
but using "by simp" displays the informations written with pwriteln
(Pretty.writeln) in the response buffer together. is this something "by"
does?
The regular way to output things is via writeln. In some situations,
end-of-proof (e.g. via 'by') prints a result using writeln as well. In an
open proof state, some extra workarounds are required, because most Proof
General configurations tend to put the state output in front. You should
be able to switch back to *response* nonetheless, or use "3 window mode"
or something.
If you look at print_tac in the sources, it uses tracing explicitly,
hoping to escape these traps. There are other variations on the theme,
like using warning, or even the special Output.priority protocol message.
The latter is generally a bit dangerous, because it suppresses error
output in certain situations, causing great confusion.
All of this is very fragile, and will only become better with the next
generation of user interfaces. As a general rule of thumb, one should
keep the ML part as plain and simple as possible, and use writeln most of
the time.
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.
I did not know that it can actually be run -- when I tried some years ago
I failed miserably. In my frustation I asked the Google oracle what to do
about "Eclipse sucks", and it pointed me to a blog spot saying "Do not use
Eclipse, but jEdit." Some years later, I have an almost working version
of Isabelle/jEdit. The one distributed with Isabelle2009-2 is merely a
sneak preview -- if you look closely you can imagine its full potential.
Even that partial version is already quite good to get acuainted with
Isabelle/ML programming, though. Some months ago we sucessfully ran a 2
day workshop on Isabelle tool development using this mini-IDE with great
success. E.g. hovering over ML embedded in the theory source will give
you tooltips about inferred types, or CTRL-hover-click gives you
hyperlinks to navigate the the sources. The "Output" window also shows
results from the prover without too much smartness getting in between.
See Isabelle2009-2/src/Tools/jEdit/README for further details. Assuming
you have an original (!) JVM 1.6 from Sun/Oracle, you merely need to say
"isabelle jedit" to get you out of the old PG/Emacs world order. (It is
not usable for serious proof development right now.)
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
