added Mailbox, as in ML;
authorwenzelm
Thu Apr 24 12:10:26 2014 +0200 (2014-04-24)
changeset 566930423c957b081
parent 56692 8219a65b24e3
child 56694 c4e77643aad6
added Mailbox, as in ML;
src/Pure/Concurrent/mailbox.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/mailbox.scala	Thu Apr 24 12:10:26 2014 +0200
     1.3 @@ -0,0 +1,37 @@
     1.4 +/*  Title:      Pure/Concurrent/mailbox.scala
     1.5 +    Module:     PIDE
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Message exchange via mailbox, with non-blocking send (due to unbounded
     1.9 +queueing) and potentially blocking receive.
    1.10 +*/
    1.11 +
    1.12 +package isabelle
    1.13 +
    1.14 +
    1.15 +import scala.collection.immutable.Queue
    1.16 +
    1.17 +
    1.18 +object Mailbox
    1.19 +{
    1.20 +  def apply[A]: Mailbox[A] = new Mailbox[A]()
    1.21 +}
    1.22 +
    1.23 +
    1.24 +class Mailbox[A] private()
    1.25 +{
    1.26 +  private val mailbox = Synchronized(Queue.empty[A])
    1.27 +  override def toString: String = mailbox.value.mkString("Mailbox(", ",", ")")
    1.28 +
    1.29 +  def send(msg: A): Unit =
    1.30 +    mailbox.change(_.enqueue(msg))
    1.31 +
    1.32 +  def receive: A =
    1.33 +    mailbox.guarded_access(_.dequeueOption)
    1.34 +
    1.35 +  def receive_timeout(timeout: Time): Option[A] =
    1.36 +    mailbox.timed_access(_ => Some(Time.now() + timeout), _.dequeueOption)
    1.37 +
    1.38 +  def await_empty: Unit =
    1.39 +    mailbox.guarded_access(queue => if (queue.isEmpty) Some(((), queue)) else None)
    1.40 +}
     2.1 --- a/src/Pure/build-jars	Thu Apr 24 12:09:55 2014 +0200
     2.2 +++ b/src/Pure/build-jars	Thu Apr 24 12:10:26 2014 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  declare -a SOURCES=(
     2.5    Concurrent/counter.scala
     2.6    Concurrent/future.scala
     2.7 +  Concurrent/mailbox.scala
     2.8    Concurrent/simple_thread.scala
     2.9    Concurrent/synchronized.scala
    2.10    General/antiquote.scala