| author | wenzelm |
| Fri, 17 Jul 2015 16:43:53 +0200 | |
| changeset 60745 | d86b4cd0f1ec |
| parent 56303 | 4cc3f4db3447 |
| child 62357 | ab76bd43c14a |
| 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.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 -- generic 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 |
signature EXN_OUTPUT = |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
8 |
sig |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
9 |
val position: exn -> Position.T |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
10 |
val pretty: exn -> Pretty.T |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
11 |
end |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
12 |
|
|
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) = Position.none |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
17 |
val pretty = Pretty.str o General.exnMessage; |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
18 |
|
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
19 |
end; |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
diff
changeset
|
20 |