src/Pure/System/event_bus.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 45673 cd41e3903fbf
child 55618 995162143ef4
permissions -rw-r--r--
more official command specifications, including source position;
     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 }