Hi all,

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).

This is Isabelle/jEdit.

Should this work? Is there something else I should use?

Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to