# HG changeset patch
# User wenzelm
# Date 1237803646 -3600
# Node ID d6248d4508d5b38f8ffd1127f536b34991d2d79c
# Parent  4cf38ea4fad2416168c1a5a15f28db569bfb137c
future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;

diff -r 4cf38ea4fad2 -r d6248d4508d5 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Mar 23 08:16:24 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Mon Mar 23 11:20:46 2009 +0100
@@ -212,7 +212,8 @@
     val _ = if continue then () else scheduler := NONE;
 
     val _ = notify_all ();
-    val _ = interruptible (fn () => wait_timeout (Time.fromSeconds 1)) ()
+    val _ = interruptible (fn () =>
+        wait_timeout (Time.fromMilliseconds (if null (! canceled) then 1000 else 50))) ()
       handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
   in continue end;