[isabelle-dev] Debugging low-level exceptions
krauss at in.tum.de
Fri Mar 15 22:48:02 CET 2013
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
Runtime.debug := true;
does not seem to have any effect (or I did not look in the right place).
This is Isabelle/jEdit.
Should this work? Is there something else I should use?
More information about the isabelle-dev