| author | blanchet |
| Wed, 17 Feb 2016 11:54:34 +0100 | |
| changeset 62326 | 3cf7a067599c |
| parent 56303 | 4cc3f4db3447 |
| child 62354 | fdd6989cc8a0 |
| permissions | -rw-r--r-- |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/exn_output_polyml.ML |
|
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 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
4 |
Auxiliary operations for exception output -- Poly/ML version. |
|
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 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
7 |
structure Exn_Output: EXN_OUTPUT = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
8 |
struct |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
9 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
10 |
fun position exn = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
11 |
(case PolyML.exceptionLocation exn of |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
12 |
NONE => Position.none |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
13 |
| SOME loc => Exn_Properties.position_of loc); |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
14 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
15 |
fun pretty (exn: exn) = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
16 |
Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ()))); |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
17 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
18 |
end; |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
19 |