| author | wenzelm |
| Thu, 17 Dec 2015 17:32:01 +0100 | |
| changeset 61862 | e2a9e46ac0fb |
| parent 59470 | 31d810570879 |
| permissions | -rw-r--r-- |
| 59470 | 1 |
(* Title: Pure/ML-Systems/exn_trace_polyml-5.5.1.ML |
|
52836
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 |
|
| 59470 | 4 |
Exception trace for Poly/ML 5.5.1 via ML output. |
|
52836
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 |
|
|
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
56283
diff
changeset
|
7 |
fun print_exception_trace exn_message output 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; |
| 59470 | 12 |
val _ = output (String.concatWith "\n" (title :: trace)); |
|
52836
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 |