| author | wenzelm |
| Tue, 01 Mar 2016 22:11:36 +0100 | |
| changeset 62494 | b90109b2487c |
| parent 62387 | ad3eb2889f9a |
| child 62503 | 19afb533028e |
| permissions | -rw-r--r-- |
| 62355 | 1 |
(* Title: Pure/ML/exn_output.ML |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
3 |
|
| 62355 | 4 |
Auxiliary operations for exception output. |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
6 |
|
| 62354 | 7 |
signature EXN_OUTPUT = |
8 |
sig |
|
9 |
val position: exn -> Position.T |
|
10 |
val pretty: exn -> Pretty.T |
|
11 |
end; |
|
12 |
||
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
13 |
structure Exn_Output: EXN_OUTPUT = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
14 |
struct |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
15 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
16 |
fun position exn = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
17 |
(case PolyML.exceptionLocation exn of |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
18 |
NONE => Position.none |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
19 |
| SOME loc => Exn_Properties.position_of loc); |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
20 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
21 |
fun pretty (exn: exn) = |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62357
diff
changeset
|
22 |
Pretty.from_ML |
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62357
diff
changeset
|
23 |
(pretty_ml |
|
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62357
diff
changeset
|
24 |
(PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ())))); |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
25 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
26 |
end; |