# HG changeset patch
# User wenzelm
# Date 1313612700 -7200
# Node ID 6a3541412b23bb0742fb6e8dca5f3c5c573d580a
# Parent  270366301bd7ff8d35f04100cbee7fd2b86935cb
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;

diff -r 270366301bd7 -r 6a3541412b23 src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:14:22 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:25:00 2011 +0200
@@ -42,8 +42,13 @@
   if all_res results then map Exn.release results
   else raise make (map_filter Exn.get_exn results);
 
-fun release_first results = release_all results
-  handle Par_Exn ((serial, exn) :: _) => reraise exn;  (* FIXME preserve serial in location (?!?) *)
+fun release_first results =
+  if all_res results then map Exn.release results
+  else
+    (case get_first
+        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
+      NONE => Exn.interrupt ()
+    | SOME exn => reraise exn);
 
 end;