interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
authorwenzelm
Tue, 28 Jul 2009 14:11:15 +0200
changeset 322513e7d1673f96e
parent 32250 d4f7934e9555
child 32252 0241916a5f06
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 28 14:04:33 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 28 14:11:15 2009 +0200
     1.3 @@ -401,11 +401,12 @@
     1.4  
     1.5  fun interruptible_task f x =
     1.6    if Multithreading.available then
     1.7 +   (Thread.testInterrupt ();
     1.8      Multithreading.with_attributes
     1.9        (if is_worker ()
    1.10         then Multithreading.restricted_interrupts
    1.11         else Multithreading.regular_interrupts)
    1.12 -      (fn _ => f) x
    1.13 +      (fn _ => fn x => f x) x)
    1.14    else interruptible f x;
    1.15  
    1.16  (*cancel: present and future group members will be interrupted eventually*)