[isabelle-dev] NEWS: improved printing of exception trace in Poly/ML 5.5.1

Makarius makarius at sketis.net
Wed Sep 18 21:23:29 CEST 2013

*** ML ***

* Improved printing of exception trace in Poly/ML 5.5.1, with regular
tracing output in the command transaction context instead of physical
stdout.  See also Toplevel.debug, Toplevel.debugging and

This refers to Isabelle/84522727f9d3.

Documented ways for experimental debugging in Isabelle/ML are now:

    Toplevel.debug (or Toplevel.debugging)



So this is another opportunity to give up raw PolyML.exception_trace and 
PolyML.makestring.  This is bright and shining Isabelle/ML, not some "ML 
level of Isabelle" in dark cellars.

There is actually more that could be done: activating the runtime debugger 
of Poly/ML within Isabelle/ML and its IDE.  It is probably not that 
difficult, but we have the release looming, and I had to waste so much 
time explaining that there is no "ML level of Isabelle".  Hopefully this 
will not come up again.


More information about the isabelle-dev mailing list