equal
deleted
inserted
replaced
41 |
41 |
42 fun par_exns (Par_Exn exns) = exns |
42 fun par_exns (Par_Exn exns) = exns |
43 | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)]; |
43 | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)]; |
44 |
44 |
45 fun make exns = |
45 fun make exns = |
46 (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of |
46 (case Ord_List.unions exn_ord (map par_exns exns) of |
47 [] => Exn.Interrupt |
47 [] => Exn.Interrupt |
48 | es => Par_Exn es); |
48 | es => Par_Exn es); |
49 |
49 |
50 fun dest (Par_Exn exns) = SOME exns |
50 fun dest (Par_Exn exns) = SOME exns |
51 | dest exn = if Exn.is_interrupt exn then SOME [] else NONE; |
51 | dest exn = if Exn.is_interrupt exn then SOME [] else NONE; |