# HG changeset patch
# User wenzelm
# Date 1230571653 -3600
# Node ID 787ba47201c79a8afc43364b9be7a4fc8763f4f9
# Parent  de62fdd4b4321da917877f53b3bad008d7ea2f80
optional exception logging;
tuned comments;

diff -r de62fdd4b432 -r 787ba47201c7 src/Pure/General/event_bus.scala
--- a/src/Pure/General/event_bus.scala	Mon Dec 29 16:45:00 2008 +0100
+++ b/src/Pure/General/event_bus.scala	Mon Dec 29 18:27:33 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) }
+    }
+  }
 }