For some time Makarius has been asking for a way for PolyML.exception_trace to be able to output the trace through an ML function rather than directly to stdout. I've now added PolyML.Exception.traceException. At the same time I've moved the various functions related to exceptions into PolyML.Exception although for the time being they are still available directly in PolyML.
traceException has the signature val traceException = fn: (unit -> 'a) * (string list * exn -> 'a) -> 'a
The first argument is the function to run and if this returns without an exception the result is returned from traceException. If it raises an exception the second argument is called with the trace and the original exception. This can then reraise the exception after producing the trace or return a default result. As always I can and may change it before the next release.
By the way, it requires the updated compiler so it isn't there until "make compiler" has been run.
David