src/Pure/Concurrent/mailbox.scala
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61590 94ab348eaab2
child 64370 865b39487b5d
permissions -rw-r--r--
proper syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Concurrent/mailbox.scala
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     2
    Module:     PIDE
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     4
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
     5
Message exchange via mailbox, with multiple senders (non-blocking,
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
     6
unbounded buffering) and single receiver (bulk messages).
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     7
*/
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     8
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
     9
package isabelle
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    10
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    11
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    12
object Mailbox
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    13
{
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    14
  def apply[A]: Mailbox[A] = new Mailbox[A]()
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    15
}
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    16
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    17
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    18
class Mailbox[A] private()
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    19
{
61590
wenzelm
parents: 57417
diff changeset
    20
  private val mailbox = Synchronized[List[A]](Nil)
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    21
  override def toString: String = mailbox.value.reverse.mkString("Mailbox(", ",", ")")
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    22
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    23
  def send(msg: A): Unit = mailbox.change(msg :: _)
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    24
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    25
  def receive(timeout: Option[Time]): List[A] =
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    26
    (mailbox.timed_access(_ => timeout.map(t => Time.now() + t),
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    27
      { case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    28
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    29
  def await_empty: Unit =
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56693
diff changeset
    30
    mailbox.guarded_access({ case Nil => Some(((), Nil)) case _ => None })
56693
0423c957b081 added Mailbox, as in ML;
wenzelm
parents:
diff changeset
    31
}