src/Pure/ML/exn_properties_polyml.ML
changeset 56303 4cc3f4db3447
parent 50911 ee7fe4230642
child 58714 ca0b7d7cc9a3
     1.1 --- a/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature EXN_PROPERTIES =
     1.6  sig
     1.7 -  val of_location: PolyML.location -> Properties.T
     1.8 +  val position_of: PolyML.location -> Position.T
     1.9    val get: exn -> Properties.T
    1.10    val update: Properties.entry list -> exn -> exn
    1.11  end;
    1.12 @@ -14,23 +14,35 @@
    1.13  structure Exn_Properties: EXN_PROPERTIES =
    1.14  struct
    1.15  
    1.16 -fun of_location (loc: PolyML.location) =
    1.17 +(* source locations *)
    1.18 +
    1.19 +fun props_of (loc: PolyML.location) =
    1.20    (case YXML.parse_body (#file loc) of
    1.21      [] => []
    1.22    | [XML.Text file] => [(Markup.fileN, file)]
    1.23    | body => XML.Decode.properties body);
    1.24  
    1.25 +fun position_of loc =
    1.26 +  Position.make
    1.27 +   {line = #startLine loc,
    1.28 +    offset = #startPosition loc,
    1.29 +    end_offset = #endPosition loc,
    1.30 +    props = props_of loc};
    1.31 +
    1.32 +
    1.33 +(* exception properties *)
    1.34 +
    1.35  fun get exn =
    1.36    (case PolyML.exceptionLocation exn of
    1.37      NONE => []
    1.38 -  | SOME loc => of_location loc);
    1.39 +  | SOME loc => props_of loc);
    1.40  
    1.41  fun update entries exn =
    1.42    let
    1.43      val loc =
    1.44        the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    1.45          (PolyML.exceptionLocation exn);
    1.46 -    val props = of_location loc;
    1.47 +    val props = props_of loc;
    1.48      val props' = fold Properties.put entries props;
    1.49    in
    1.50      if props = props' then exn