src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26254 3def1a1fea4e
parent 26221 e557c20158e2
child 26390 99d4cbb1f941
equal deleted inserted replaced
26253:0506197d285f 26254:3def1a1fea4e
   310       | fork k = (start worker; fork (k - 1));
   310       | fork k = (start worker; fork (k - 1));
   311     val _ = PROTECTED "main" (fn () =>
   311     val _ = PROTECTED "main" (fn () =>
   312      (fork (Int.max (n, 1));
   312      (fork (Int.max (n, 1));
   313       while not (List.null (! running)) do
   313       while not (List.null (! running)) do
   314       (trace_active ();
   314       (trace_active ();
   315        if not (List.null (! status)) then (List.app Thread.interrupt (! running)) else ();
   315        if not (List.null (! status))
       
   316        then (List.app (fn t => Thread.interrupt t handle Thread _ => ()) (! running))
       
   317        else ();
   316        wait_timeout ())));
   318        wait_timeout ())));
   317 
   319 
   318   in ! status end);
   320   in ! status end);
   319 
   321 
   320 
   322