1(* Title: Pure/ML/exn_properties.ML 2 Author: Makarius 3 4Exception properties. 5*) 6 7signature EXN_PROPERTIES = 8sig 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 13end; 14 15structure Exn_Properties: EXN_PROPERTIES = 16struct 17 18(* source locations *) 19 20fun 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 28fun 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 35fun 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 43fun get exn = 44 (case Exn.polyml_location exn of 45 NONE => [] 46 | SOME loc => props_of_polyml_location loc); 47 48fun 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 71end; 72