schedule main control: more robust interrupting of potentially running threads;
authorwenzelm
Tue, 11 Mar 2008 20:30:46 +0100
changeset 26254 3def1a1fea4e
parent 26253 0506197d285f
child 26255 2246d8bbe89d
schedule main control: more robust interrupting of potentially running threads;
src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 11 19:35:05 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 11 20:30:46 2008 +0100
@@ -312,7 +312,9 @@
      (fork (Int.max (n, 1));
       while not (List.null (! running)) do
       (trace_active ();
-       if not (List.null (! status)) then (List.app Thread.interrupt (! running)) else ();
+       if not (List.null (! status))
+       then (List.app (fn t => Thread.interrupt t handle Thread _ => ()) (! running))
+       else ();
        wait_timeout ())));
 
   in ! status end);