# HG changeset patch
# User wenzelm
# Date 1257423382 -3600
# Node ID 13d00799fe49d8f8972235f27cb219865237275b
# Parent  352fe8e9162d56c3dae23edd9243f0daf7bc2313
scheduler: clarified interrupt attributes and handling;

diff -r 352fe8e9162d -r 13d00799fe49 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Nov 05 13:01:11 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Nov 05 13:16:22 2009 +0100
@@ -337,13 +337,14 @@
   in continue end
   handle Exn.Interrupt =>
    (Multithreading.tracing 1 (fn () => "Interrupt");
-    uninterruptible (fn _ => fn () => List.app do_cancel (Task_Queue.cancel_all (! queue))) ();
-    scheduler_next ());
+    List.app do_cancel (Task_Queue.cancel_all (! queue)); true);
 
 fun scheduler_loop () =
-  Multithreading.with_attributes
-    (Multithreading.sync_interrupts Multithreading.public_interrupts)
-    (fn _ => while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ());
+  while
+    Multithreading.with_attributes
+      (Multithreading.sync_interrupts Multithreading.public_interrupts)
+      (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
+  do ();
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);