equal
deleted
inserted
replaced
27 val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial); |
27 val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial); |
28 |
28 |
29 |
29 |
30 (* parallel exceptions *) |
30 (* parallel exceptions *) |
31 |
31 |
32 exception Par_Exn of exn Ord_List.T; |
32 exception Par_Exn of exn list; |
|
33 (*non-empty list with unique identified elements sorted by exn_ord; |
|
34 no occurrences of Par_Exn or Exn.Interrupt*) |
33 |
35 |
34 fun par_exns (Par_Exn exns) = SOME exns |
36 fun par_exns (Par_Exn exns) = exns |
35 | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)]; |
37 | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)]; |
36 |
38 |
37 fun make exns = |
39 fun make exns = |
38 (case map_filter par_exns exns of |
40 (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of |
39 [] => Exn.Interrupt |
41 [] => Exn.Interrupt |
40 | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es))); |
42 | es => Par_Exn es); |
41 |
43 |
42 fun dest (Par_Exn exns) = SOME (rev exns) |
44 fun dest (Par_Exn exns) = SOME exns |
43 | dest _ = NONE; |
45 | dest _ = NONE; |
44 |
46 |
45 |
47 |
46 (* parallel results *) |
48 (* parallel results *) |
47 |
49 |