*** 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
ML_Compiler.exn_trace.
This refers to Isabelle/84522727f9d3.
Documented ways for experimental debugging in Isabelle/ML are now:
Toplevel.debug (or Toplevel.debugging)
ML_Compiler.exn_trace
@{make_string}
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
