[isabelle-dev] Debugging low-level exceptions
krauss at in.tum.de
Mon Mar 18 23:33:55 CET 2013
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.
More information about the isabelle-dev