# HG changeset patch
# User wenzelm
# Date 1230555457 -3600
# Node ID 89217ccfd1305d2ff31329be57af5e626d5fed3b
# Parent  ff41885a12346968d25fb38d9ebea7725eea979c
Generic event bus.

diff -r ff41885a1234 -r 89217ccfd130 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) }
+}
diff -r ff41885a1234 -r 89217ccfd130 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Dec 28 14:41:47 2008 -0800
+++ b/src/Pure/IsaMakefile	Mon Dec 29 13:57:37 2008 +0100
@@ -121,10 +121,11 @@
 
 ## Scala material
 
-SCALA_FILES = General/markup.scala General/position.scala		\
-  General/symbol.scala General/xml.scala General/yxml.scala		\
-  Isar/isar.scala Thy/thy_header.scala Tools/isabelle_process.scala	\
-  Tools/isabelle_syntax.scala Tools/isabelle_system.scala
+SCALA_FILES = General/event_bus.scala General/markup.scala	\
+  General/position.scala General/symbol.scala General/xml.scala	\
+  General/yxml.scala Isar/isar.scala Thy/thy_header.scala	\
+  Tools/isabelle_process.scala Tools/isabelle_syntax.scala	\
+  Tools/isabelle_system.scala
 
 
 SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar