# HG changeset patch # User wenzelm # Date 1220818798 -7200 # Node ID 96cbf4afdc7d7527029791f97ec13f7ee19c331f # Parent 0435d23deccc2fcd11dd8863011a93492335df09 tuned; diff -r 0435d23deccc -r 96cbf4afdc7d src/Pure/Concurrent/mailbox.ML --- a/src/Pure/Concurrent/mailbox.ML Sun Sep 07 22:19:46 2008 +0200 +++ b/src/Pure/Concurrent/mailbox.ML Sun Sep 07 22:19:58 2008 +0200 @@ -53,13 +53,7 @@ ConditionVar.waitUntil (cond, lock, limit) andalso check (); val ok = restore_attributes check () handle Interrupt => (Mutex.unlock lock; raise Interrupt); - val res = - if ok then - let - val (msg, msgs) = Queue.dequeue (! messages); - val _ = messages := msgs; - in SOME msg end - else NONE; + val res = if ok then SOME (change_result messages Queue.dequeue) else NONE; val _ = Mutex.unlock lock; in res end) (); 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 ())))));