# HG changeset patch
# User wenzelm
# Date 1347442703 -7200
# Node ID f4b91a3a5f0f105f5561f9020140e29600e779fb
# Parent  612a04e7c853a47a3eb1a553207470c81d4f59bf
more robust interrupt handling;

diff -r 612a04e7c853 -r f4b91a3a5f0f src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed Sep 12 11:28:34 2012 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Sep 12 11:38:23 2012 +0200
@@ -33,14 +33,17 @@
       not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
   then map (Exn.capture f) xs
   else
-    let
-      val group = Future.new_group (Future.worker_group ());
-      val futures =
-        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
-          (map (fn x => fn () => f x) xs);
-      val results = Future.join_results futures
-        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
-    in results end;
+    uninterruptible (fn restore_attributes => fn () =>
+      let
+        val group = Future.new_group (Future.worker_group ());
+        val futures =
+          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
+            (map (fn x => fn () => f x) xs);
+        val results =
+          restore_attributes Future.join_results futures
+            handle exn =>
+              (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+      in results end) ();
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
 fun map f = map_name "Par_List.map" f;