added methods "+" and "-";
event: non-synchronized execution of handlers, based on synchronized snapshot;

--- 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))
 }