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