1(*  Title:      Pure/ML/exn_properties.ML
2    Author:     Makarius
3
4Exception properties.
5*)
6
7signature EXN_PROPERTIES =
8sig
9  val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
10  val position: exn -> Position.T
11  val get: exn -> Properties.T
12  val update: Properties.entry list -> exn -> exn
13end;
14
15structure Exn_Properties: EXN_PROPERTIES =
16struct
17
18(* source locations *)
19
20fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
21  (case YXML.parse_body (#file loc) of
22    [] => []
23  | [XML.Text file] =>
24      if file = "Standard Basis" then []
25      else [(Markup.fileN, ML_System.standard_path file)]
26  | body => XML.Decode.properties body);
27
28fun position_of_polyml_location loc =
29  Position.make
30   {line = FixedInt.toInt (#startLine loc),
31    offset = FixedInt.toInt (#startPosition loc),
32    end_offset = FixedInt.toInt (#endPosition loc),
33    props = props_of_polyml_location loc};
34
35fun position exn =
36  (case Exn.polyml_location exn of
37    NONE => Position.none
38  | SOME loc => position_of_polyml_location loc);
39
40
41(* exception properties *)
42
43fun get exn =
44  (case Exn.polyml_location exn of
45    NONE => []
46  | SOME loc => props_of_polyml_location loc);
47
48fun update entries exn =
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}
54          (Exn.polyml_location exn);
55      val props = props_of_polyml_location loc;
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
66          Thread_Attributes.uninterruptible (fn _ => fn () =>
67            PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
68        end
69    end;
70
71end;
72