src/Pure/ML/exn_properties.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62923 3a122e1e352a
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62355
     1
(*  Title:      Pure/ML/exn_properties.ML
wenzelm@50911
     2
    Author:     Makarius
wenzelm@50911
     3
wenzelm@62355
     4
Exception properties.
wenzelm@50911
     5
*)
wenzelm@50911
     6
wenzelm@50911
     7
signature EXN_PROPERTIES =
wenzelm@50911
     8
sig
wenzelm@62821
     9
  val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
wenzelm@62516
    10
  val position: exn -> Position.T
wenzelm@50911
    11
  val get: exn -> Properties.T
wenzelm@50911
    12
  val update: Properties.entry list -> exn -> exn
wenzelm@50911
    13
end;
wenzelm@50911
    14
wenzelm@50911
    15
structure Exn_Properties: EXN_PROPERTIES =
wenzelm@50911
    16
struct
wenzelm@50911
    17
wenzelm@56303
    18
(* source locations *)
wenzelm@56303
    19
wenzelm@62821
    20
fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
wenzelm@50911
    21
  (case YXML.parse_body (#file loc) of
wenzelm@50911
    22
    [] => []
wenzelm@58714
    23
  | [XML.Text file] =>
wenzelm@58714
    24
      if file = "Standard Basis" then []
wenzelm@62468
    25
      else [(Markup.fileN, ML_System.standard_path file)]
wenzelm@50911
    26
  | body => XML.Decode.properties body);
wenzelm@50911
    27
wenzelm@62821
    28
fun position_of_polyml_location loc =
wenzelm@56303
    29
  Position.make
wenzelm@62387
    30
   {line = FixedInt.toInt (#startLine loc),
wenzelm@62387
    31
    offset = FixedInt.toInt (#startPosition loc),
wenzelm@62387
    32
    end_offset = FixedInt.toInt (#endPosition loc),
wenzelm@62821
    33
    props = props_of_polyml_location loc};
wenzelm@62516
    34
wenzelm@62516
    35
fun position exn =
wenzelm@62821
    36
  (case Exn.polyml_location exn of
wenzelm@62516
    37
    NONE => Position.none
wenzelm@62821
    38
  | SOME loc => position_of_polyml_location loc);
wenzelm@56303
    39
wenzelm@56303
    40
wenzelm@56303
    41
(* exception properties *)
wenzelm@56303
    42
wenzelm@50911
    43
fun get exn =
wenzelm@62821
    44
  (case Exn.polyml_location exn of
wenzelm@50911
    45
    NONE => []
wenzelm@62821
    46
  | SOME loc => props_of_polyml_location loc);
wenzelm@50911
    47
wenzelm@50911
    48
fun update entries exn =
wenzelm@62518
    49
  if Exn.is_interrupt exn then exn
wenzelm@62518
    50
  else
wenzelm@62518
    51
    let
wenzelm@62518
    52
      val loc =
wenzelm@62518
    53
        the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
wenzelm@62821
    54
          (Exn.polyml_location exn);
wenzelm@62821
    55
      val props = props_of_polyml_location loc;
wenzelm@62518
    56
      val props' = fold Properties.put entries props;
wenzelm@62518
    57
    in
wenzelm@62518
    58
      if props = props' then exn
wenzelm@62518
    59
      else
wenzelm@62518
    60
        let
wenzelm@62518
    61
          val loc' =
wenzelm@62518
    62
            {file = YXML.string_of_body (XML.Encode.properties props'),
wenzelm@62518
    63
              startLine = #startLine loc, endLine = #endLine loc,
wenzelm@62518
    64
              startPosition = #startPosition loc, endPosition = #endPosition loc};
wenzelm@62518
    65
        in
wenzelm@62923
    66
          Thread_Attributes.uninterruptible (fn _ => fn () =>
wenzelm@62518
    67
            PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
wenzelm@62518
    68
        end
wenzelm@62518
    69
    end;
wenzelm@50911
    70
wenzelm@50911
    71
end;