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).
Hope this helps,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
