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

[Makarius]

*** 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