| author | wenzelm |
| Mon, 05 Aug 2013 15:03:52 +0200 | |
| changeset 52861 | e93d73b51fd0 |
| parent 52836 | 1a03ffc00a4a |
| child 53709 | 84522727f9d3 |
| 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 |
|
|
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
7 |
fun exception_trace e = |
|
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 |
|
1a03ffc00a4a
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
wenzelm
parents:
diff
changeset
|
11 |
val title = "Exception trace - " ^ ML_Compiler.exn_message exn; |
|
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 |