src/Pure/ML/exn_trace_polyml-5.5.1.ML
author wenzelm
Wed Nov 26 14:35:55 2014 +0100 (2014-11-26 ago)
changeset 59055 5a7157b8e870
parent 56283 20cf88cd3188
permissions -rw-r--r--
more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
     1 (*  Title:      Pure/ML/exn_trace_polyml-5.5.1.ML
     2     Author:     Makarius
     3 
     4 Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
     5 *)
     6 
     7 fun print_exception_trace exn_message output e =
     8   PolyML.Exception.traceException
     9     (e, fn (trace, exn) =>
    10       let
    11         val title = "Exception trace - " ^ exn_message exn;
    12         val _ = output (cat_lines (title :: trace));
    13       in reraise exn end);
    14 
    15 PolyML.Compiler.reportExhaustiveHandlers := true;
    16