tuned;
authorwenzelm
Sun, 07 Sep 2008 22:19:58 +0200
changeset 28158 96cbf4afdc7d
parent 28157 0435d23deccc
child 28159 80823c582b9d
tuned;
src/Pure/Concurrent/mailbox.ML
src/Pure/Concurrent/schedule.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) ();
--- 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 ())))));