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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
