src/Pure/ML/exn_properties_polyml.ML
author wenzelm
Mon Oct 20 10:19:50 2014 +0200 (2014-10-20)
changeset 58714 ca0b7d7cc9a3
parent 56303 4cc3f4db3447
child 61138 dcbec1b22b07
permissions -rw-r--r--
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
     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] =>
    23       if file = "Standard Basis" then []
    24       else [(Markup.fileN, file)]
    25   | body => XML.Decode.properties body);
    26 
    27 fun position_of loc =
    28   Position.make
    29    {line = #startLine loc,
    30     offset = #startPosition loc,
    31     end_offset = #endPosition loc,
    32     props = props_of loc};
    33 
    34 
    35 (* exception properties *)
    36 
    37 fun get exn =
    38   (case PolyML.exceptionLocation exn of
    39     NONE => []
    40   | SOME loc => props_of loc);
    41 
    42 fun update entries exn =
    43   let
    44     val loc =
    45       the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    46         (PolyML.exceptionLocation exn);
    47     val props = props_of loc;
    48     val props' = fold Properties.put entries props;
    49   in
    50     if props = props' then exn
    51     else
    52       let
    53         val loc' =
    54           {file = YXML.string_of_body (XML.Encode.properties props'),
    55             startLine = #startLine loc, endLine = #endLine loc,
    56             startPosition = #startPosition loc, endPosition = #endPosition loc};
    57       in
    58         uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    59           handle exn' => exn'
    60       end
    61   end;
    62 
    63 end;
    64