src/Pure/Concurrent/future.ML
changeset 59330 cb3a4caf206d
parent 59180 c0fa3b3bdabd
child 59338 2ea1bf517842
equal deleted inserted replaced
59329:72278d083d3a 59330:cb3a4caf206d
   262     NONE => ()
   262     NONE => ()
   263   | SOME work => (worker_exec work; worker_loop name));
   263   | SOME work => (worker_exec work; worker_loop name));
   264 
   264 
   265 fun worker_start name = (*requires SYNCHRONIZED*)
   265 fun worker_start name = (*requires SYNCHRONIZED*)
   266   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
   266   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
   267     Unsynchronized.ref Working));
   267     Unsynchronized.ref Working))
       
   268   handle Fail msg => Multithreading.tracing 0 (fn () => msg);
       
   269 
   268 
   270 
   269 
   271 
   270 (* scheduler *)
   272 (* scheduler *)
   271 
   273 
   272 fun scheduler_next () = (*requires SYNCHRONIZED*)
   274 fun scheduler_next () = (*requires SYNCHRONIZED*)