[isabelle-dev] Supported Poly/ML versions

[Makarius]

On Sat, 13 Feb 2016, Lars Hupel 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.
>
> IMHO this sounds too obscure to be useful. How many users are actually 
> aware of that possibility?

Maybe 2-3 people on this mailing list, but this is only a guess. So lets 
make a constructive proof and count the people who show up here to say 
that they knew that already.

It is indeed all very obscure.  Time is better invested in making the 
Poly/ML 5.6 debugger work for the Pure bootstrap as well, and add some 
explicit support for exceptions to it.


 	Makarius