# HG changeset patch
# User wenzelm
# Date 1248783075 -7200
# Node ID 3e7d1673f96e5397a64c5b49470f158735141376
# Parent  d4f7934e95551d5e29cf6628cda69c825a898800
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);

diff -r d4f7934e9555 -r 3e7d1673f96e src/Pure/Concurrent/future.ML
--- 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*)