future scheduler: uninterruptible cancelation;
authorwenzelm
Sat, 01 Aug 2009 00:17:03 +0200
changeset 32296 e6a8ed8aed3a
parent 32295 400cc493d466
child 32300 ad33af3242f3
future scheduler: uninterruptible cancelation;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Aug 01 00:09:45 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 01 00:17:03 2009 +0200
@@ -285,10 +285,9 @@
   in continue end
   handle Exn.Interrupt =>
    (Multithreading.tracing 1 (fn () => "Interrupt");
-    List.app do_cancel (Task_Queue.cancel_all (! queue));
+    uninterruptible (fn _ => fn () => List.app do_cancel (Task_Queue.cancel_all (! queue))) ();
     scheduler_next ());
 
-
 fun scheduler_loop () =
   Multithreading.with_attributes
     (Multithreading.sync_interrupts Multithreading.public_interrupts)