author | wenzelm |
Fri, 27 Mar 2020 22:01:27 +0100 | |
changeset 71601 | 97ccf48c2f0c |
parent 71250 | bd93c71521a0 |
child 77776 | 58e53c61f15f |
permissions | -rw-r--r-- |
62355 | 1 |
(* Title: Pure/ML/exn_properties.ML |
50911
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 |
|
62355 | 4 |
Exception properties. |
50911
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 |
62821 | 9 |
val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T |
62516 | 10 |
val position: exn -> Position.T |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
11 |
val get: exn -> Properties.T |
71250 | 12 |
val update: Properties.T -> exn -> exn |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
13 |
end; |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
14 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
15 |
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
|
16 |
struct |
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
17 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
18 |
(* source locations *) |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
19 |
|
62821 | 20 |
fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) = |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
21 |
(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
|
22 |
[] => [] |
58714
ca0b7d7cc9a3
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents:
56303
diff
changeset
|
23 |
| [XML.Text file] => |
ca0b7d7cc9a3
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
wenzelm
parents:
56303
diff
changeset
|
24 |
if file = "Standard Basis" then [] |
62468 | 25 |
else [(Markup.fileN, ML_System.standard_path file)] |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
26 |
| 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
|
27 |
|
62821 | 28 |
fun position_of_polyml_location loc = |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
29 |
Position.make |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62355
diff
changeset
|
30 |
{line = FixedInt.toInt (#startLine loc), |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62355
diff
changeset
|
31 |
offset = FixedInt.toInt (#startPosition loc), |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62355
diff
changeset
|
32 |
end_offset = FixedInt.toInt (#endPosition loc), |
62821 | 33 |
props = props_of_polyml_location loc}; |
62516 | 34 |
|
35 |
fun position exn = |
|
62821 | 36 |
(case Exn.polyml_location exn of |
62516 | 37 |
NONE => Position.none |
62821 | 38 |
| SOME loc => position_of_polyml_location loc); |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
39 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
40 |
|
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
41 |
(* exception properties *) |
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
50911
diff
changeset
|
42 |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
43 |
fun get exn = |
62821 | 44 |
(case Exn.polyml_location exn of |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
45 |
NONE => [] |
62821 | 46 |
| SOME loc => props_of_polyml_location loc); |
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
47 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
48 |
fun update entries exn = |
62518 | 49 |
if Exn.is_interrupt exn then exn |
50 |
else |
|
51 |
let |
|
52 |
val loc = |
|
53 |
the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
|
62821 | 54 |
(Exn.polyml_location exn); |
55 |
val props = props_of_polyml_location loc; |
|
62518 | 56 |
val props' = fold Properties.put entries props; |
57 |
in |
|
58 |
if props = props' then exn |
|
59 |
else |
|
60 |
let |
|
61 |
val loc' = |
|
62 |
{file = YXML.string_of_body (XML.Encode.properties props'), |
|
63 |
startLine = #startLine loc, endLine = #endLine loc, |
|
64 |
startPosition = #startPosition loc, endPosition = #endPosition loc}; |
|
65 |
in |
|
62923 | 66 |
Thread_Attributes.uninterruptible (fn _ => fn () => |
62518 | 67 |
PolyML.raiseWithLocation (exn, loc') handle exn' => exn') () |
68 |
end |
|
69 |
end; |
|
50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
70 |
|
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents:
diff
changeset
|
71 |
end; |