src/Pure/General/event_bus.scala
author wenzelm
Mon Dec 29 18:27:33 2008 +0100 (2008-12-29)
changeset 29200 787ba47201c7
parent 29191 de56edf88514
child 32539 668052c4220e
permissions -rw-r--r--
optional exception logging;
tuned comments;
wenzelm@29190
     1
/*  Title:      Pure/General/event_bus.scala
wenzelm@29190
     2
    Author:     Makarius
wenzelm@29190
     3
wenzelm@29200
     4
Generic event bus with multiple handlers and optional exception
wenzelm@29200
     5
logging.
wenzelm@29190
     6
*/
wenzelm@29190
     7
wenzelm@29190
     8
package isabelle
wenzelm@29190
     9
wenzelm@29191
    10
import scala.collection.mutable.ListBuffer
wenzelm@29190
    11
wenzelm@29190
    12
wenzelm@29200
    13
class EventBus[Event]
wenzelm@29200
    14
{
wenzelm@29200
    15
  /* event handlers */
wenzelm@29200
    16
wenzelm@29190
    17
  type Handler = Event => Unit
wenzelm@29191
    18
  private val handlers = new ListBuffer[Handler]
wenzelm@29190
    19
wenzelm@29191
    20
  def += (h: Handler) = synchronized { handlers += h }
wenzelm@29191
    21
  def + (h: Handler) = { this += h; this }
wenzelm@29191
    22
wenzelm@29190
    23
  def -= (h: Handler) = synchronized { handlers -= h }
wenzelm@29191
    24
  def - (h: Handler) = { this -= h; this }
wenzelm@29190
    25
wenzelm@29200
    26
wenzelm@29200
    27
  /* event invocation */
wenzelm@29200
    28
wenzelm@29200
    29
  var logger: Throwable => Unit = throw _
wenzelm@29200
    30
wenzelm@29200
    31
  def event(x: Event) = {
wenzelm@29200
    32
    val log = logger
wenzelm@29200
    33
    for (h <- synchronized { handlers.toList }) {
wenzelm@29200
    34
      try { h(x) }
wenzelm@29200
    35
      catch { case e: Throwable => log(e) }
wenzelm@29200
    36
    }
wenzelm@29200
    37
  }
wenzelm@29190
    38
}