diff -r 0435d23deccc -r 96cbf4afdc7d src/Pure/Concurrent/schedule.ML --- a/src/Pure/Concurrent/schedule.ML Sun Sep 07 22:19:46 2008 +0200 +++ b/src/Pure/Concurrent/schedule.ML Sun Sep 07 22:19:58 2008 +0200 @@ -42,24 +42,20 @@ fun trace_active () = Multithreading.tracing 1 (fn () => "SCHEDULE: " ^ string_of_int (! active) ^ " active"); fun dequeue () = - let - val (next, tasks') = next_task (! queue); - val _ = queue := tasks'; - in - (case next of Wait => + (case change_result queue next_task of + Wait => (dec active; trace_active (); wait (); inc active; trace_active (); dequeue ()) - | _ => next) - end; + | next => next); (*pool of running threads*) val status = ref ([]: exn list); val running = ref ([]: Thread.thread list); fun start f = (inc active; - change running (cons (Thread.fork (f, [Thread.InterruptState Thread.InterruptDefer])))); + change running (cons (Thread.fork (f, Multithreading.no_interrupts)))); fun stop () = (dec active; change running (filter (fn t => not (Thread.equal (t, Thread.self ())))));