[isabelle-dev] Supported Poly/ML versions
makarius at sketis.net
Sat Feb 13 15:25:39 CET 2016
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
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.
More information about the isabelle-dev