src/Pure/Concurrent/future.ML
changeset 32247 3e7d1673f96e
parent 32246 d4f7934e9555
child 32248 0241916a5f06
--- a/src/Pure/Concurrent/future.ML	Tue Jul 28 14:04:33 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Jul 28 14:11:15 2009 +0200
@@ -401,11 +401,12 @@
 
 fun interruptible_task f x =
   if Multithreading.available then
+   (Thread.testInterrupt ();
     Multithreading.with_attributes
       (if is_worker ()
        then Multithreading.restricted_interrupts
        else Multithreading.regular_interrupts)
-      (fn _ => f) x
+      (fn _ => fn x => f x) x)
   else interruptible f x;
 
 (*cancel: present and future group members will be interrupted eventually*)