future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
1.1 --- a/src/Pure/Concurrent/future.ML Mon Mar 23 08:16:24 2009 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Mon Mar 23 11:20:46 2009 +0100
1.3 @@ -212,7 +212,8 @@
1.4 val _ = if continue then () else scheduler := NONE;
1.5
1.6 val _ = notify_all ();
1.7 - val _ = interruptible (fn () => wait_timeout (Time.fromSeconds 1)) ()
1.8 + val _ = interruptible (fn () =>
1.9 + wait_timeout (Time.fromMilliseconds (if null (! canceled) then 1000 else 50))) ()
1.10 handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
1.11 in continue end;
1.12