| author | boehmes |
| Thu, 01 May 2014 22:56:59 +0200 | |
| changeset 56815 | 848d507584db |
| 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 |