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