# HG changeset patch
# User wenzelm
# Date 1230571805 -3600
# Node ID 03908107bc5b54c95733fb4e3ddead3d1e62afe8
# Parent  69b806be5a0aa66cb74c696c8cfd126d359de2cf# Parent  787ba47201c79a8afc43364b9be7a4fc8763f4f9
merged

diff -r 69b806be5a0a -r 03908107bc5b src/Pure/General/event_bus.scala
--- a/src/Pure/General/event_bus.scala	Mon Dec 29 17:57:18 2008 +0100
+++ b/src/Pure/General/event_bus.scala	Mon Dec 29 18:30:05 2008 +0100
@@ -1,7 +1,8 @@
 /*  Title:      Pure/General/event_bus.scala
     Author:     Makarius
 
-Generic event bus.
+Generic event bus with multiple handlers and optional exception
+logging.
 */
 
 package isabelle
@@ -9,7 +10,10 @@
 import scala.collection.mutable.ListBuffer
 
 
-class EventBus[Event] {
+class EventBus[Event]
+{
+  /* event handlers */
+
   type Handler = Event => Unit
   private val handlers = new ListBuffer[Handler]
 
@@ -19,5 +23,16 @@
   def -= (h: Handler) = synchronized { handlers -= h }
   def - (h: Handler) = { this -= h; this }
 
-  def event(e: Event) = synchronized { handlers.toList } foreach (h => h(e))
+
+  /* event invocation */
+
+  var logger: Throwable => Unit = throw _
+
+  def event(x: Event) = {
+    val log = logger
+    for (h <- synchronized { handlers.toList }) {
+      try { h(x) }
+      catch { case e: Throwable => log(e) }
+    }
+  }
 }