equal
deleted
inserted
replaced
1 (* Title: Pure/ML/exn_output.ML |
|
2 Author: Makarius |
|
3 |
|
4 Auxiliary operations for exception output. |
|
5 *) |
|
6 |
|
7 signature EXN_OUTPUT = |
|
8 sig |
|
9 val position: exn -> Position.T |
|
10 val pretty: exn -> Pretty.T |
|
11 end; |
|
12 |
|
13 structure Exn_Output: EXN_OUTPUT = |
|
14 struct |
|
15 |
|
16 fun position exn = |
|
17 (case PolyML.exceptionLocation exn of |
|
18 NONE => Position.none |
|
19 | SOME loc => Exn_Properties.position_of loc); |
|
20 |
|
21 fun pretty (exn: exn) = |
|
22 Pretty.from_ML |
|
23 (ML_Pretty.from_polyml |
|
24 (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ())))); |
|
25 |
|
26 end; |
|