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