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