# HG changeset patch
# User wenzelm
# Date 1249078623 -7200
# Node ID e6a8ed8aed3ad61e7f3bbf6060b6683136086a81
# Parent  400cc493d4666776fff7d74ec585039477e76bf0
future scheduler: uninterruptible cancelation;

diff -r 400cc493d466 -r e6a8ed8aed3a 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)