future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
authorwenzelm
Mon, 23 Mar 2009 11:20:46 +0100
changeset 30666d6248d4508d5
parent 30665 4cf38ea4fad2
child 30667 53fbf7c679b0
future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
src/Pure/Concurrent/future.ML
     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