jEdit looks very good! i will i try it the next days, but from what what i experienced during five minutes, i think i will keep it. thanks for your answer /Nils
2010/9/8 Makarius <[email protected]>: > 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
