clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
authorwenzelm
Thu Aug 18 15:39:00 2011 +0200 (2011-08-18)
changeset 44266d9c7bf932eab
parent 44265 b94951f06e48
child 44267 d4d48d75aac3
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
src/Pure/Concurrent/par_exn.ML
     1.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:37:01 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 15:39:00 2011 +0200
     1.3 @@ -47,19 +47,19 @@
     1.4  
     1.5  (* parallel results *)
     1.6  
     1.7 -fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
     1.8 +fun release_all results =
     1.9 +  if forall (fn Exn.Res _ => true | _ => false) results
    1.10 +  then map Exn.release results
    1.11 +  else raise make (map_filter Exn.get_exn results);
    1.12  
    1.13 -fun release_all results =
    1.14 -  if all_res results then map Exn.release results
    1.15 -  else raise make (map_filter Exn.get_exn results);
    1.16 +fun plain_exn (Exn.Res _) = NONE
    1.17 +  | plain_exn (Exn.Exn (Par_Exn _)) = NONE
    1.18 +  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
    1.19  
    1.20  fun release_first results =
    1.21 -  if all_res results then map Exn.release results
    1.22 -  else
    1.23 -    (case get_first
    1.24 -        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
    1.25 -      NONE => Exn.interrupt ()
    1.26 -    | SOME exn => reraise exn);
    1.27 +  (case get_first plain_exn results of
    1.28 +    NONE => release_all results
    1.29 +  | SOME exn => reraise exn);
    1.30  
    1.31  end;
    1.32