interruptible: Thread.testInterrupt before changing thread attributes;

--- a/src/Pure/Concurrent/future.ML	Mon Jul 27 17:12:19 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jul 27 17:36:30 2009 +0200
@@ -165,9 +165,10 @@
       let
         val res =
           if ok then
-            Exn.capture
-              (Multithreading.with_attributes Multithreading.restricted_interrupts
-                (fn _ => fn () => e ())) ()
+            Exn.capture (fn () =>
+             (Thread.testInterrupt ();
+              Multithreading.with_attributes Multithreading.restricted_interrupts
+                (fn _ => fn () => e ())) ()) ()
           else Exn.Exn Exn.Interrupt;
         val _ = result := SOME res;
       in
@@ -282,7 +283,9 @@
     val delay =
       Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
     val _ = wait_interruptible scheduler_event delay
-      handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
+      handle Exn.Interrupt =>
+        (Multithreading.tracing 1 (fn () => "Interrupt");
+          List.app do_cancel (Task_Queue.cancel_all (! queue)));
 
     (*shutdown*)
     val _ = if Task_Queue.is_empty (! queue) then do_shutdown := true else ();

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 27 17:12:19 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 27 17:36:30 2009 +0200
@@ -110,8 +110,8 @@
     val _ = Thread.setAttributes orig_atts;
   in Exn.release result end;
 
-fun interruptible f =
-  with_attributes regular_interrupts (fn _ => fn x => f x);
+fun interruptible f x =
+  (Thread.testInterrupt (); with_attributes regular_interrupts (fn _ => fn x => f x) x);
 
 fun uninterruptible f =
   with_attributes no_interrupts (fn atts => fn x =>