src/Pure/Concurrent/future.ML
changeset 32230 9f6461b1c9cc
parent 32229 abdc0f6214c8
child 32246 d4f7934e9555
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 27 17:12:19 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 17:36:30 2009 +0200
     1.3 @@ -165,9 +165,10 @@
     1.4        let
     1.5          val res =
     1.6            if ok then
     1.7 -            Exn.capture
     1.8 -              (Multithreading.with_attributes Multithreading.restricted_interrupts
     1.9 -                (fn _ => fn () => e ())) ()
    1.10 +            Exn.capture (fn () =>
    1.11 +             (Thread.testInterrupt ();
    1.12 +              Multithreading.with_attributes Multithreading.restricted_interrupts
    1.13 +                (fn _ => fn () => e ())) ()) ()
    1.14            else Exn.Exn Exn.Interrupt;
    1.15          val _ = result := SOME res;
    1.16        in
    1.17 @@ -282,7 +283,9 @@
    1.18      val delay =
    1.19        Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
    1.20      val _ = wait_interruptible scheduler_event delay
    1.21 -      handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
    1.22 +      handle Exn.Interrupt =>
    1.23 +        (Multithreading.tracing 1 (fn () => "Interrupt");
    1.24 +          List.app do_cancel (Task_Queue.cancel_all (! queue)));
    1.25  
    1.26      (*shutdown*)
    1.27      val _ = if Task_Queue.is_empty (! queue) then do_shutdown := true else ();