src/Pure/General/event_bus.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/event_bus.scala	Mon Dec 29 13:57:37 2008 +0100
@@ -0,0 +1,20 @@
+/*  Title:      Pure/General/event_bus.scala
+    Author:     Makarius
+
+Generic event bus.
+*/
+
+package isabelle
+
+import scala.collection.jcl.LinkedList
+
+
+class EventBus[Event] {
+  type Handler = Event => Unit
+  private val handlers = new LinkedList[Handler]
+
+  def += (h: Handler) = synchronized { handlers -= h; handlers += h }
+  def -= (h: Handler) = synchronized { handlers -= h }
+
+  def event(e: Event) = synchronized { for(h <- handlers) h(e) }
+}