[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.


More information about the isabelle-dev mailing list