src/Pure/Concurrent/mailbox.ML

--- a/src/Pure/Concurrent/mailbox.ML	Wed Jul 10 22:04:57 2013 +0200
+++ b/src/Pure/Concurrent/mailbox.ML	Wed Jul 10 22:56:48 2013 +0200
@@ -12,6 +12,7 @@
   val send: 'a T -> 'a -> unit
   val receive: 'a T -> 'a
   val receive_timeout: Time.time -> 'a T -> 'a option
+  val await_empty: 'a T -> unit
 end;
 
 structure Mailbox: MAILBOX =
@@ -31,4 +32,8 @@
   Synchronized.timed_access mailbox
     (fn _ => SOME (Time.+ (Time.now (), timeout))) (try Queue.dequeue);
 
+fun await_empty (Mailbox mailbox) =
+  Synchronized.guarded_access mailbox
+    (fn queue => if Queue.is_empty queue then SOME ((), queue) else NONE);
+
 end;