--- a/src/Pure/Concurrent/mailbox.scala Fri Jun 27 19:38:32 2014 +0200
+++ b/src/Pure/Concurrent/mailbox.scala Fri Jun 27 22:08:55 2014 +0200
@@ -2,16 +2,13 @@
Module: PIDE
Author: Makarius
-Message exchange via mailbox, with non-blocking send (due to unbounded
-queueing) and potentially blocking receive.
+Message exchange via mailbox, with multiple senders (non-blocking,
+unbounded buffering) and single receiver (bulk messages).
*/
package isabelle
-import scala.collection.immutable.Queue
-
-
object Mailbox
{
def apply[A]: Mailbox[A] = new Mailbox[A]()
@@ -20,18 +17,15 @@
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))
+ private val mailbox = Synchronized(List.empty[A])
+ override def toString: String = mailbox.value.reverse.mkString("Mailbox(", ",", ")")
- def receive: A =
- mailbox.guarded_access(_.dequeueOption)
+ def send(msg: A): Unit = mailbox.change(msg :: _)
- def receive_timeout(timeout: Time): Option[A] =
- mailbox.timed_access(_ => Some(Time.now() + timeout), _.dequeueOption)
+ def receive(timeout: Option[Time]): List[A] =
+ (mailbox.timed_access(_ => timeout.map(t => Time.now() + t),
+ { case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse
def await_empty: Unit =
- mailbox.guarded_access(queue => if (queue.isEmpty) Some(((), queue)) else None)
+ mailbox.guarded_access({ case Nil => Some(((), Nil)) case _ => None })
}