> On 14.02.2016, at 02:22, Makarius <makar...@sketis.net> wrote: > > 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.
I agree. No need from my side to hold on to the older polyml versions. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
