[isabelle-dev] Debugging low-level exceptions

[Makarius]

On Sat, 16 Mar 2013, Florian Haftmann wrote:

> Hi Alex,
>
>> What is the current (as of, say, d5c95b55f849) method for getting
>> exception traces? I am trying to debug a low-level exception such as
>>
>>   exception Match raised (line 287 of "term.ML")
>>
>> which happens somewhere below partial_function. Some years ago there
>> used to be "Toplevel.debug" flag, which would activate printing traces
>> of any top-level errors. The closest to this I found in the current
>> codebase is "Runtime.debug : bool Unsynchronized.ref", but putting
>>
>> ML {*
>>   Runtime.debug := true;
>> *}
>>
>> does not seem to have any effect (or I did not look in the right place).
>
> 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.


 	Makarius