[isabelle-dev] Isabelle/jEdit and Toplevel.debug
Makarius
makarius at sketis.net
Tue Feb 14 23:14:06 CET 2012
On Sat, 11 Feb 2012, Florian Haftmann wrote:
> In plain old tty days one would get a traceback for exceptions atfer
>
> ML {* Toplevel.debug := true *}
>
> Is this trace somehow accessible by jEdit also?
It is on the same low-level stdout channel as on the TTY or Proof General,
but this is also the reason why it is less accessible in the Prover IDE --
due to lack of Isabelle/Isar transaction context.
Isabelle/jEdit provides a "Raw Output" panel for such physical process
output, which is a bit awkward but not more than going back to TTY.
Makarius
More information about the isabelle-dev
mailing list