src/Pure/System/event_bus.scala
author wenzelm
Thu Feb 20 14:36:17 2014 +0100 (2014-02-20)
changeset 55618 995162143ef4
parent 45673 cd41e3903fbf
child 56686 2386d1a3ca8f
permissions -rw-r--r--
tuned imports;
     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 
    11 import scala.actors.Actor, Actor._
    12 import scala.collection.mutable.ListBuffer
    13 
    14 
    15 class Event_Bus[Event]
    16 {
    17   /* receivers */
    18 
    19   private val receivers = new ListBuffer[Actor]
    20 
    21   def += (r: Actor) { synchronized { receivers += r } }
    22   def + (r: Actor): Event_Bus[Event] = { this += r; this }
    23 
    24   def += (f: Event => Unit) {
    25     this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
    26   }
    27 
    28   def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
    29 
    30   def -= (r: Actor) { synchronized { receivers -= r } }
    31   def - (r: Actor) = { this -= r; this }
    32 
    33 
    34   /* event invocation */
    35 
    36   def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
    37 }