1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 19 12:03:44 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 12:51:14 2011 +0200
     1.3 @@ -174,13 +174,14 @@
     1.4  (* cancellation primitives *)
     1.5  
     1.6  fun interruptible_task f x =
     1.7 -  if Multithreading.available then
     1.8 +  (if Multithreading.available then
     1.9      Multithreading.with_attributes
    1.10        (if is_some (worker_task ())
    1.11         then Multithreading.private_interrupts
    1.12         else Multithreading.public_interrupts)
    1.13        (fn _ => f x)
    1.14 -  else interruptible f x;
    1.15 +   else interruptible f x)
    1.16 +  before Multithreading.interrupted ();
    1.17  
    1.18  fun cancel_now group = (*requires SYNCHRONIZED*)
    1.19    Task_Queue.cancel (! queue) group;
    1.20 @@ -209,9 +210,9 @@
    1.21      val _ = SYNCHRONIZED "finish" (fn () =>
    1.22        let
    1.23          val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
    1.24 -        val _ = Exn.capture Multithreading.interrupted ();
    1.25 +        val test = Exn.capture Multithreading.interrupted ();
    1.26          val _ =
    1.27 -          if ok then ()
    1.28 +          if ok andalso not (Exn.is_interrupt_exn test) then ()
    1.29            else if cancel_now group then ()
    1.30            else cancel_later group;
    1.31          val _ = broadcast work_finished;
    1.32 @@ -245,7 +246,7 @@
    1.33  fun worker_loop name =
    1.34    (case SYNCHRONIZED name (fn () => worker_next ()) of
    1.35      NONE => ()
    1.36 -  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
    1.37 +  | SOME work => (worker_exec work; worker_loop name));
    1.38  
    1.39  fun worker_start name = (*requires SYNCHRONIZED*)
    1.40    Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
    1.41 @@ -431,8 +432,7 @@
    1.42                Multithreading.with_attributes
    1.43                  (if interrupts
    1.44                   then Multithreading.private_interrupts else Multithreading.no_interrupts)
    1.45 -                (fn _ => Position.setmp_thread_data pos e ()) before
    1.46 -              Multithreading.interrupted ()) ()
    1.47 +                (fn _ => Position.setmp_thread_data pos e ())) ()
    1.48            else Exn.interrupt_exn;
    1.49        in assign_result group result res end;
    1.50    in (result, job) end;