| changeset 61925 | ab52f183f020 |
| parent 61924 | 55b3d21ab5e5 |
| child 61926 | 17ba31a2303b |
| 61924:55b3d21ab5e5 | 61925:ab52f183f020 |
|---|---|
1 (* Title: Pure/ML-Systems/exn_trace_polyml-5.5.1.ML |
|
2 Author: Makarius |
|
3 |
|
4 Exception trace for Poly/ML 5.5.1 via ML output. |
|
5 *) |
|
6 |
|
7 fun print_exception_trace exn_message output e = |
|
8 PolyML.Exception.traceException |
|
9 (e, fn (trace, exn) => |
|
10 let |
|
11 val title = "Exception trace - " ^ exn_message exn; |
|
12 val _ = output (String.concatWith "\n" (title :: trace)); |
|
13 in reraise exn end); |
|
14 |
|
15 PolyML.Compiler.reportExhaustiveHandlers := true; |
|
16 |