[isabelle-dev] Methods that fail with stack-overflow

[Lars Noschinski]

On 03.07.2014 13:57, Peter Lammich wrote:
> Hi,
>
> I recently ran into a method that produced a stack-overflow.
>
> The good thing is: In the current jedit version, it is properly
> highlighted and you immediately see that there is some error. (This was
> not always the case in the past)
>
> The bad thing: The only way how to get a clue what is going wrong is to
> open the "raw output panel". This writes "stack-overflow" then, without
> any location or trace. How to enable tracing for those exceptions, in
> particular as Toplevel.debug seems to have gone away?
There is ML_trace (and a similar option); i.e. "declare [[ML_trace]]".
Have a look at print_options. I don't know whether this helps in your
concrete situation.