author | wenzelm |
Fri, 27 Jun 2014 22:08:55 +0200 | |
changeset 57417 | 29fe9bac501b |
parent 56693 | 0423c957b081 |
child 61590 | 94ab348eaab2 |
permissions | -rw-r--r-- |
56693 | 1 |
/* Title: Pure/Concurrent/mailbox.scala |
2 |
Module: PIDE |
|
3 |
Author: Makarius |
|
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 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
12 |
object Mailbox |
|
13 |
{ |
|
14 |
def apply[A]: Mailbox[A] = new Mailbox[A]() |
|
15 |
} |
|
16 |
||
17 |
||
18 |
class Mailbox[A] private() |
|
19 |
{ |
|
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
20 |
private val mailbox = Synchronized(List.empty[A]) |
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 | 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 | 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 | 28 |
|
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 | 31 |
} |