[isabelle-dev] NEWS: improved printing of exception trace in Poly/ML 5.5.1
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