author | wenzelm |
Sun, 28 Feb 2016 21:20:51 +0100 | |
changeset 62459 | 7a5d88dd8cc9 |
parent 61925 | src/Pure/RAW/exn_trace_polyml-5.5.1.ML@ab52f183f020 |
permissions | -rw-r--r-- |
(* Title: Pure/RAW/exn_trace.ML Author: Makarius Exception trace via ML output, for Poly/ML 5.5.1 or later. *) 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;