interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
--- 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*)