src/Pure/System/event_bus.scala
author wenzelm
Sun Aug 15 23:13:56 2010 +0200 (2010-08-15)
changeset 38428 c13c95c97e89
parent 36676 src/Pure/PIDE/event_bus.scala@ac7961d42ac3
child 38849 2f198d107aef
permissions -rw-r--r--
event_bus.scala rather belongs to system plumbing;
wenzelm@38428
     1
/*  Title:      Pure/System/event_bus.scala
wenzelm@29190
     2
    Author:     Makarius
wenzelm@29190
     3
wenzelm@32539
     4
Generic event bus with multiple receiving actors.
wenzelm@29190
     5
*/
wenzelm@29190
     6
wenzelm@29190
     7
package isabelle
wenzelm@29190
     8
wenzelm@32539
     9
import scala.actors.Actor, Actor._
wenzelm@29191
    10
import scala.collection.mutable.ListBuffer
wenzelm@29190
    11
wenzelm@29190
    12
wenzelm@32539
    13
class Event_Bus[Event]
wenzelm@29200
    14
{
wenzelm@32539
    15
  /* receivers */
wenzelm@32539
    16
wenzelm@32539
    17
  private val receivers = new ListBuffer[Actor]
wenzelm@32539
    18
wenzelm@32539
    19
  def += (r: Actor) { synchronized { receivers += r } }
wenzelm@32539
    20
  def + (r: Actor): Event_Bus[Event] = { this += r; this }
wenzelm@29200
    21
wenzelm@32539
    22
  def += (f: Event => Unit) {
wenzelm@32539
    23
    this += actor { loop { react { case x: Event => f(x) } } }
wenzelm@32539
    24
  }
wenzelm@29190
    25
wenzelm@32539
    26
  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
wenzelm@29191
    27
wenzelm@32539
    28
  def -= (r: Actor) { synchronized { receivers -= r } }
wenzelm@32539
    29
  def - (r: Actor) = { this -= r; this }
wenzelm@29190
    30
wenzelm@29200
    31
wenzelm@29200
    32
  /* event invocation */
wenzelm@29200
    33
wenzelm@32539
    34
  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
wenzelm@29190
    35
}