src/Pure/ML/exn_properties_polyml.ML
author wenzelm
Wed Jan 16 16:26:36 2013 +0100 (2013-01-16)
changeset 50911 ee7fe4230642
child 56303 4cc3f4db3447
permissions -rw-r--r--
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
     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 of_location: PolyML.location -> Properties.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 fun of_location (loc: PolyML.location) =
    18   (case YXML.parse_body (#file loc) of
    19     [] => []
    20   | [XML.Text file] => [(Markup.fileN, file)]
    21   | body => XML.Decode.properties body);
    22 
    23 fun get exn =
    24   (case PolyML.exceptionLocation exn of
    25     NONE => []
    26   | SOME loc => of_location loc);
    27 
    28 fun update entries exn =
    29   let
    30     val loc =
    31       the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    32         (PolyML.exceptionLocation exn);
    33     val props = of_location loc;
    34     val props' = fold Properties.put entries props;
    35   in
    36     if props = props' then exn
    37     else
    38       let
    39         val loc' =
    40           {file = YXML.string_of_body (XML.Encode.properties props'),
    41             startLine = #startLine loc, endLine = #endLine loc,
    42             startPosition = #startPosition loc, endPosition = #endPosition loc};
    43       in
    44         uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    45           handle exn' => exn'
    46       end
    47   end;
    48 
    49 end;
    50