src/Pure/Concurrent/future.ML
changeset 34281 eedea6f0b37e
parent 34280 16bf3e9786a3
child 35016 c0f2e49bccfc
equal deleted inserted replaced
34280:16bf3e9786a3 34281:eedea6f0b37e
   503        else Multithreading.public_interrupts)
   503        else Multithreading.public_interrupts)
   504       (fn _ => f x)
   504       (fn _ => f x)
   505   else interruptible f x;
   505   else interruptible f x;
   506 
   506 
   507 (*cancel: present and future group members will be interrupted eventually*)
   507 (*cancel: present and future group members will be interrupted eventually*)
   508 fun cancel_group group = SYNCHRONIZED "cancel" (fn () => cancel_later group);
   508 fun cancel_group group =
       
   509   SYNCHRONIZED "cancel" (fn () => if cancel_now group then () else cancel_later group);
   509 fun cancel x = cancel_group (group_of x);
   510 fun cancel x = cancel_group (group_of x);
   510 
   511 
   511 
   512 
   512 (* shutdown *)
   513 (* shutdown *)
   513 
   514