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);
wenzelm@52836
     1
(*  Title:      Pure/ML/exn_trace_polyml-5.5.1.ML
wenzelm@52836
     2
    Author:     Makarius
wenzelm@52836
     3
wenzelm@52836
     4
Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
wenzelm@52836
     5
*)
wenzelm@52836
     6
wenzelm@59055
     7
fun print_exception_trace exn_message output e =
wenzelm@52836
     8
  PolyML.Exception.traceException
wenzelm@52836
     9
    (e, fn (trace, exn) =>
wenzelm@52836
    10
      let
wenzelm@53709
    11
        val title = "Exception trace - " ^ exn_message exn;
wenzelm@59055
    12
        val _ = output (cat_lines (title :: trace));
wenzelm@52836
    13
      in reraise exn end);
wenzelm@52836
    14
wenzelm@56283
    15
PolyML.Compiler.reportExhaustiveHandlers := true;
wenzelm@56283
    16