equal
deleted
inserted
replaced
45 | dest _ = NONE; |
45 | dest _ = NONE; |
46 |
46 |
47 |
47 |
48 (* parallel results *) |
48 (* parallel results *) |
49 |
49 |
50 fun all_res results = forall (fn Exn.Res _ => true | _ => false) results; |
|
51 |
|
52 fun release_all results = |
50 fun release_all results = |
53 if all_res results then map Exn.release results |
51 if forall (fn Exn.Res _ => true | _ => false) results |
|
52 then map Exn.release results |
54 else raise make (map_filter Exn.get_exn results); |
53 else raise make (map_filter Exn.get_exn results); |
55 |
54 |
|
55 fun plain_exn (Exn.Res _) = NONE |
|
56 | plain_exn (Exn.Exn (Par_Exn _)) = NONE |
|
57 | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn; |
|
58 |
56 fun release_first results = |
59 fun release_first results = |
57 if all_res results then map Exn.release results |
60 (case get_first plain_exn results of |
58 else |
61 NONE => release_all results |
59 (case get_first |
62 | SOME exn => reraise exn); |
60 (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of |
|
61 NONE => Exn.interrupt () |
|
62 | SOME exn => reraise exn); |
|
63 |
63 |
64 end; |
64 end; |
65 |
65 |