|
1 (* Title: Pure/ML/exn_properties.ML |
|
2 Author: Makarius |
|
3 |
|
4 Exception properties. |
|
5 *) |
|
6 |
|
7 signature EXN_PROPERTIES = |
|
8 sig |
|
9 val position_of: PolyML.location -> Position.T |
|
10 val get: exn -> Properties.T |
|
11 val update: Properties.entry list -> exn -> exn |
|
12 end; |
|
13 |
|
14 structure Exn_Properties: EXN_PROPERTIES = |
|
15 struct |
|
16 |
|
17 (* source locations *) |
|
18 |
|
19 fun props_of (loc: PolyML.location) = |
|
20 (case YXML.parse_body (#file loc) of |
|
21 [] => [] |
|
22 | [XML.Text file] => |
|
23 if file = "Standard Basis" then [] |
|
24 else [(Markup.fileN, ml_standard_path file)] |
|
25 | body => XML.Decode.properties body); |
|
26 |
|
27 fun position_of loc = |
|
28 Position.make |
|
29 {line = #startLine loc, |
|
30 offset = #startPosition loc, |
|
31 end_offset = #endPosition loc, |
|
32 props = props_of loc}; |
|
33 |
|
34 |
|
35 (* exception properties *) |
|
36 |
|
37 fun get exn = |
|
38 (case PolyML.exceptionLocation exn of |
|
39 NONE => [] |
|
40 | SOME loc => props_of loc); |
|
41 |
|
42 fun update entries exn = |
|
43 let |
|
44 val loc = |
|
45 the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
|
46 (PolyML.exceptionLocation exn); |
|
47 val props = props_of loc; |
|
48 val props' = fold Properties.put entries props; |
|
49 in |
|
50 if props = props' then exn |
|
51 else |
|
52 let |
|
53 val loc' = |
|
54 {file = YXML.string_of_body (XML.Encode.properties props'), |
|
55 startLine = #startLine loc, endLine = #endLine loc, |
|
56 startPosition = #startPosition loc, endPosition = #endPosition loc}; |
|
57 in |
|
58 uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) () |
|
59 handle exn' => exn' |
|
60 end |
|
61 end; |
|
62 |
|
63 end; |