46 (case Exn.polyml_location exn of |
46 (case Exn.polyml_location exn of |
47 NONE => [] |
47 NONE => [] |
48 | SOME loc => props_of_polyml_location loc); |
48 | SOME loc => props_of_polyml_location loc); |
49 |
49 |
50 fun update entries exn = |
50 fun update entries exn = |
51 if Exn.is_interrupt exn then exn |
51 let |
52 else |
52 val loc = |
53 let |
53 the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
54 val loc = |
54 (Exn.polyml_location exn); |
55 the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
55 val props = props_of_polyml_location loc; |
56 (Exn.polyml_location exn); |
56 val props' = fold Properties.put entries props; |
57 val props = props_of_polyml_location loc; |
57 in |
58 val props' = fold Properties.put entries props; |
58 if props = props' then exn |
59 in |
59 else |
60 if props = props' then exn |
60 let |
61 else |
61 val loc' = |
62 let |
62 {file = YXML.string_of_body (XML.Encode.properties props'), |
63 val loc' = |
63 startLine = #startLine loc, endLine = #endLine loc, |
64 {file = YXML.string_of_body (XML.Encode.properties props'), |
64 startPosition = #startPosition loc, endPosition = #endPosition loc}; |
65 startLine = #startLine loc, endLine = #endLine loc, |
65 in |
66 startPosition = #startPosition loc, endPosition = #endPosition loc}; |
66 Thread_Attributes.uninterruptible (fn _ => fn () => |
67 in |
67 PolyML.raiseWithLocation (exn, loc') handle exn' => exn') () |
68 Thread_Attributes.uninterruptible (fn _ => fn () => |
68 end |
69 PolyML.raiseWithLocation (exn, loc') handle exn' => exn') () |
69 end; |
70 end |
|
71 end; |
|
72 |
70 |
73 |
71 |
74 (* identification via serial numbers *) |
72 (* identification via serial numbers *) |
75 |
73 |
76 fun identify default_props exn = |
74 fun identify default_props exn = |
77 let |
75 if Exn.is_interrupt exn then exn |
78 val props = get exn; |
76 else |
79 val update_serial = |
77 let |
80 if Properties.defined props Markup.serialN then [] |
78 val props = get exn; |
81 else [(Markup.serialN, serial_string ())]; |
79 val update_serial = |
82 val update_props = filter_out (Properties.defined props o #1) default_props; |
80 if Properties.defined props Markup.serialN then [] |
83 in update (update_serial @ update_props) exn end; |
81 else [(Markup.serialN, serial_string ())]; |
|
82 val update_props = filter_out (Properties.defined props o #1) default_props; |
|
83 in update (update_serial @ update_props) exn end; |
84 |
84 |
85 fun the_serial exn = |
85 fun the_serial exn = |
86 Value.parse_int (the (Properties.get (get exn) Markup.serialN)); |
86 Value.parse_int (the (Properties.get (get exn) Markup.serialN)); |
87 |
87 |
88 val ord = rev_order o int_ord o apply2 the_serial; |
88 val ord = rev_order o int_ord o apply2 the_serial; |