equal
deleted
inserted
replaced
59 |
59 |
60 fun exn_msgs context exn = |
60 fun exn_msgs context exn = |
61 if Exn.is_interrupt exn then [] |
61 if Exn.is_interrupt exn then [] |
62 else |
62 else |
63 (case Par_Exn.dest exn of |
63 (case Par_Exn.dest exn of |
64 SOME exns => maps (exn_msgs context) exns |
64 SOME exns => maps (exn_msgs context) (rev exns) |
65 | NONE => |
65 | NONE => |
66 (case exn of |
66 (case exn of |
67 Exn.EXCEPTIONS exns => maps (exn_msgs context) exns |
67 Exn.EXCEPTIONS exns => maps (exn_msgs context) exns |
68 | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn |
68 | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn |
69 | EXCURSION_FAIL (exn, loc) => |
69 | EXCURSION_FAIL (exn, loc) => |