[isabelle-dev] Supported Poly/ML versions

[Makarius]

On Sat, 13 Feb 2016, Lawrence Paulson wrote:

> A pity that even this one is necessary. Has tracing somehow got worse 
> since then, and can’t that be reversed?
>
>> On 13 Feb 2016, at 13:42, Makarius <makarius at sketis.net> wrote:
>>
>>  * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a
>>    detailed exception trace. Note that this needs to be done with
>>    isabelle_process or isabelle console, since PIDE requires socket I/O
>>    and Poly/ML 5.3.0 does not work with that anymore.

Some years ago David Matthews simplified the treatment of exceptions in 
the run-time system, to reduce the overhead. As a consequence of that, a 
partial "handle" already counts like a total one, i.e. the trace is 
truncated there.

Asking David the same question as above, he pointed out that the debugger 
can do this and much more. It only needs to be wrapped-up for actual use.


 	Makarius