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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
