44 (case PolyML.exceptionLocation exn of |
44 (case PolyML.exceptionLocation exn of |
45 NONE => [] |
45 NONE => [] |
46 | SOME loc => props_of_location loc); |
46 | SOME loc => props_of_location loc); |
47 |
47 |
48 fun update entries exn = |
48 fun update entries exn = |
49 let |
49 if Exn.is_interrupt exn then exn |
50 val loc = |
50 else |
51 the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
51 let |
52 (PolyML.exceptionLocation exn); |
52 val loc = |
53 val props = props_of_location loc; |
53 the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} |
54 val props' = fold Properties.put entries props; |
54 (PolyML.exceptionLocation exn); |
55 in |
55 val props = props_of_location loc; |
56 if props = props' then exn |
56 val props' = fold Properties.put entries props; |
57 else |
57 in |
58 let |
58 if props = props' then exn |
59 val loc' = |
59 else |
60 {file = YXML.string_of_body (XML.Encode.properties props'), |
60 let |
61 startLine = #startLine loc, endLine = #endLine loc, |
61 val loc' = |
62 startPosition = #startPosition loc, endPosition = #endPosition loc}; |
62 {file = YXML.string_of_body (XML.Encode.properties props'), |
63 in |
63 startLine = #startLine loc, endLine = #endLine loc, |
64 uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) () |
64 startPosition = #startPosition loc, endPosition = #endPosition loc}; |
65 handle exn' => exn' |
65 in |
66 end |
66 uninterruptible (fn _ => fn () => |
67 end; |
67 PolyML.raiseWithLocation (exn, loc') handle exn' => exn') () |
|
68 end |
|
69 end; |
68 |
70 |
69 end; |
71 end; |