author | wenzelm |
Mon, 20 Oct 2014 10:19:50 +0200 | |
changeset 58714 | ca0b7d7cc9a3 |
parent 56303 | 4cc3f4db3447 |
child 61138 | dcbec1b22b07 |
permissions | -rw-r--r-- |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML/exn_properties_polyml.ML |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
3 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
4 |
Exception properties for Poly/ML. |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
5 |
*) |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
6 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
7 |
signature EXN_PROPERTIES = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
8 |
sig |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
9 |
val position_of: PolyML.location -> Position.T |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
10 |
val get: exn -> Properties.T |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
11 |
val update: Properties.entry list -> exn -> exn |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
12 |
end; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
13 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
14 |
structure Exn_Properties: EXN_PROPERTIES = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
15 |
struct |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
16 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
17 |
(* source locations *) |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
18 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
19 |
fun props_of (loc: PolyML.location) = |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
20 |
(case YXML.parse_body (#file loc) of |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
21 |
[] => [] |
58714
ca0b7d7cc9a3
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents:
56303
diff
changeset
|
22 |
| [XML.Text file] => |
ca0b7d7cc9a3
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents:
56303
diff
changeset
|
23 |
if file = "Standard Basis" then [] |
ca0b7d7cc9a3
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents:
56303
diff
changeset
|
24 |
else [(Markup.fileN, file)] |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
25 |
| body => XML.Decode.properties body); |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
26 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
27 |
fun position_of loc = |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
28 |
Position.make |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
29 |
{line = #startLine loc, |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
30 |
offset = #startPosition loc, |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
31 |
end_offset = #endPosition loc, |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
32 |
props = props_of loc}; |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
33 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
34 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
35 |
(* exception properties *) |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
36 |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
37 |
fun get exn = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
38 |
(case PolyML.exceptionLocation exn of |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
39 |
NONE => [] |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
40 |
| SOME loc => props_of loc); |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
41 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
42 |
fun update entries exn = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
43 |
let |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
44 |
val loc = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
45 |
the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
46 |
(PolyML.exceptionLocation exn); |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
47 |
val props = props_of loc; |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
48 |
val props' = fold Properties.put entries props; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
49 |
in |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
50 |
if props = props' then exn |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
51 |
else |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
52 |
let |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
53 |
val loc' = |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
54 |
{file = YXML.string_of_body (XML.Encode.properties props'), |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
55 |
startLine = #startLine loc, endLine = #endLine loc, |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
56 |
startPosition = #startPosition loc, endPosition = #endPosition loc}; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
57 |
in |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
58 |
uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) () |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
59 |
handle exn' => exn' |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
60 |
end |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
61 |
end; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
62 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
63 |
end; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
64 |