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;
     1 (*  Title:      Pure/ML/exn_properties_polyml.ML
     2     Author:     Makarius
     3 
     4 Exception properties for Poly/ML.
     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] => [(Markup.fileN, file)]
    23   | body => XML.Decode.properties body);
    24 
    25 fun position_of loc =
    26   Position.make
    27    {line = #startLine loc,
    28     offset = #startPosition loc,
    29     end_offset = #endPosition loc,
    30     props = props_of loc};
    31 
    32 
    33 (* exception properties *)
    34 
    35 fun get exn =
    36   (case PolyML.exceptionLocation exn of
    37     NONE => []
    38   | SOME loc => props_of loc);
    39 
    40 fun update entries exn =
    41   let
    42     val loc =
    43       the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    44         (PolyML.exceptionLocation exn);
    45     val props = props_of loc;
    46     val props' = fold Properties.put entries props;
    47   in
    48     if props = props' then exn
    49     else
    50       let
    51         val loc' =
    52           {file = YXML.string_of_body (XML.Encode.properties props'),
    53             startLine = #startLine loc, endLine = #endLine loc,
    54             startPosition = #startPosition loc, endPosition = #endPosition loc};
    55       in
    56         uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    57           handle exn' => exn'
    58       end
    59   end;
    60 
    61 end;
    62