# HG changeset patch
# User wenzelm
# Date 1230560033 -3600
# Node ID de56edf88514c9fac4bb3d7e71953126787749f1
# Parent  89217ccfd1305d2ff31329be57af5e626d5fed3b
added methods "+" and "-";
event: non-synchronized execution of handlers, based on synchronized snapshot;

diff -r 89217ccfd130 -r de56edf88514 src/Pure/General/event_bus.scala
--- a/src/Pure/General/event_bus.scala	Mon Dec 29 13:57:37 2008 +0100
+++ b/src/Pure/General/event_bus.scala	Mon Dec 29 15:13:53 2008 +0100
@@ -6,15 +6,18 @@
 
 package isabelle
 
-import scala.collection.jcl.LinkedList
+import scala.collection.mutable.ListBuffer
 
 
 class EventBus[Event] {
   type Handler = Event => Unit
-  private val handlers = new LinkedList[Handler]
+  private val handlers = new ListBuffer[Handler]
 
-  def += (h: Handler) = synchronized { handlers -= h; handlers += h }
+  def += (h: Handler) = synchronized { handlers += h }
+  def + (h: Handler) = { this += h; this }
+
   def -= (h: Handler) = synchronized { handlers -= h }
+  def - (h: Handler) = { this -= h; this }
 
-  def event(e: Event) = synchronized { for(h <- handlers) h(e) }
+  def event(e: Event) = synchronized { handlers.toList } foreach (h => h(e))
 }