--- 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 ())))));