author | hoelzl |
Wed, 02 Apr 2014 18:35:01 +0200 | |
changeset 56369 | 2704ca85be98 |
parent 56283 | 20cf88cd3188 |
child 59055 | 5a7157b8e870 |
permissions | -rw-r--r-- |
52836
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/exn_trace_polyml-5.5.1.ML |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
3 |
|
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
4 |
Exception trace for Poly/ML 5.5.1, using regular Isabelle output. |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
5 |
*) |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
6 |
|
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
52836
diff
changeset
|
7 |
fun print_exception_trace exn_message e = |
52836
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
8 |
PolyML.Exception.traceException |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
9 |
(e, fn (trace, exn) => |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
10 |
let |
53709
84522727f9d3
improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents:
52836
diff
changeset
|
11 |
val title = "Exception trace - " ^ exn_message exn; |
52836
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
12 |
val _ = tracing (cat_lines (title :: trace)); |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
13 |
in reraise exn end); |
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
14 |
|
56283
20cf88cd3188
more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);
wenzelm
parents:
53709
diff
changeset
|
15 |
PolyML.Compiler.reportExhaustiveHandlers := true; |
20cf88cd3188
more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);
wenzelm
parents:
53709
diff
changeset
|
16 |