diff -r 8219a65b24e3 -r 0423c957b081 src/Pure/Concurrent/mailbox.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/mailbox.scala	Thu Apr 24 12:10:26 2014 +0200
@@ -0,0 +1,37 @@
+/*  Title:      Pure/Concurrent/mailbox.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Message exchange via mailbox, with non-blocking send (due to unbounded
+queueing) and potentially blocking receive.
+*/
+
+package isabelle
+
+
+import scala.collection.immutable.Queue
+
+
+object Mailbox
+{
+  def apply[A]: Mailbox[A] = new Mailbox[A]()
+}
+
+
+class Mailbox[A] private()
+{
+  private val mailbox = Synchronized(Queue.empty[A])
+  override def toString: String = mailbox.value.mkString("Mailbox(", ",", ")")
+
+  def send(msg: A): Unit =
+    mailbox.change(_.enqueue(msg))
+
+  def receive: A =
+    mailbox.guarded_access(_.dequeueOption)
+
+  def receive_timeout(timeout: Time): Option[A] =
+    mailbox.timed_access(_ => Some(Time.now() + timeout), _.dequeueOption)
+
+  def await_empty: Unit =
+    mailbox.guarded_access(queue => if (queue.isEmpty) Some(((), queue)) else None)
+}