src/Pure/System/event_bus.scala
author wenzelm
Tue Nov 29 21:29:53 2011 +0100 (2011-11-29)
changeset 45673 cd41e3903fbf
parent 45667 546d78f0d81f
child 55618 995162143ef4
permissions -rw-r--r--
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
     1 /*  Title:      Pure/System/event_bus.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Generic event bus with multiple receiving actors.
     6 */
     7 
     8 package isabelle
     9 
    10 import scala.actors.Actor, Actor._
    11 import scala.collection.mutable.ListBuffer
    12 
    13 
    14 class Event_Bus[Event]
    15 {
    16   /* receivers */
    17 
    18   private val receivers = new ListBuffer[Actor]
    19 
    20   def += (r: Actor) { synchronized { receivers += r } }
    21   def + (r: Actor): Event_Bus[Event] = { this += r; this }
    22 
    23   def += (f: Event => Unit) {
    24     this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
    25   }
    26 
    27   def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
    28 
    29   def -= (r: Actor) { synchronized { receivers -= r } }
    30   def - (r: Actor) = { this -= r; this }
    31 
    32 
    33   /* event invocation */
    34 
    35   def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
    36 }