src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
author wenzelm
Thu, 17 Dec 2015 17:32:01 +0100
changeset 61862 e2a9e46ac0fb
parent 59470 31d810570879
permissions -rw-r--r--
support pretty break indent, like underlying ML systems;

(*  Title:      Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
    Author:     Makarius

Exception trace for Poly/ML 5.5.1 via ML output.
*)

fun print_exception_trace exn_message output e =
  PolyML.Exception.traceException
    (e, fn (trace, exn) =>
      let
        val title = "Exception trace - " ^ exn_message exn;
        val _ = output (String.concatWith "\n" (title :: trace));
      in reraise exn end);

PolyML.Compiler.reportExhaustiveHandlers := true;