[isabelle-dev] Debugging low-level exceptions

[Alexander Krauss]

On 03/18/2013 12:47 PM, Makarius wrote:
> On Sat, 16 Mar 2013, Florian Haftmann wrote:

>> you have to watch the »Raw output« buffer (via Plugins -> Isabelle).
>
> Toplevel.debug and Runtime.debug are the same flag, with slightly
> varying purpose over the years, but now it is just for exception_trace
> wrapping for Isar transactions.
>
> The underlying PolyML.exception_trace works via low-level stdout, so the
> "Raw Output" panel is indeed the way to see that in Isabelle/jEdit.  One
> also needs to guess what is the right trace, since it is not related to
> formal document content --- just physical output on a side-channel.

Thanks, that helped. I don't know why my first attempt didn't work (of 
course I tried raw output), but now I am getting the expected traces.

Alex