[isabelle-dev] Debugging low-level exceptions

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130316/24861935/attachment.sig>