src/Pure/PIDE/event_bus.scala
changeset 36676 ac7961d42ac3
parent 32539 668052c4220e
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/event_bus.scala	Wed May 05 22:23:45 2010 +0200
@@ -0,0 +1,35 @@
+/*  Title:      Pure/PIDE/event_bus.scala
+    Author:     Makarius
+
+Generic event bus with multiple receiving actors.
+*/
+
+package isabelle
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable.ListBuffer
+
+
+class Event_Bus[Event]
+{
+  /* receivers */
+
+  private val receivers = new ListBuffer[Actor]
+
+  def += (r: Actor) { synchronized { receivers += r } }
+  def + (r: Actor): Event_Bus[Event] = { this += r; this }
+
+  def += (f: Event => Unit) {
+    this += actor { loop { react { case x: Event => f(x) } } }
+  }
+
+  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
+
+  def -= (r: Actor) { synchronized { receivers -= r } }
+  def - (r: Actor) = { this -= r; this }
+
+
+  /* event invocation */
+
+  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
+}