| author | wenzelm |
| Wed, 04 Dec 2013 18:59:20 +0100 | |
| changeset 54667 | 4dd08fe126ba |
| parent 53709 | 84522727f9d3 |
| child 56283 | 20cf88cd3188 |
| 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 |