src/Pure/General/event_bus.scala
author wenzelm
Sat, 29 Aug 2009 14:31:39 +0200
changeset 32450 375db037f4d2
parent 29200 787ba47201c7
child 32539 668052c4220e
permissions -rw-r--r--
misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/event_bus.scala
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     3
29200
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
     4
Generic event bus with multiple handlers and optional exception
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
     5
logging.
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     6
*/
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     7
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     8
package isabelle
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     9
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    10
import scala.collection.mutable.ListBuffer
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    11
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    12
29200
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    13
class EventBus[Event]
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    14
{
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    15
  /* event handlers */
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    16
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    17
  type Handler = Event => Unit
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    18
  private val handlers = new ListBuffer[Handler]
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    19
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    20
  def += (h: Handler) = synchronized { handlers += h }
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    21
  def + (h: Handler) = { this += h; this }
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    22
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    23
  def -= (h: Handler) = synchronized { handlers -= h }
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    24
  def - (h: Handler) = { this -= h; this }
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    25
29200
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    26
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    27
  /* event invocation */
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    28
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    29
  var logger: Throwable => Unit = throw _
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    30
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    31
  def event(x: Event) = {
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    32
    val log = logger
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    33
    for (h <- synchronized { handlers.toList }) {
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    34
      try { h(x) }
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    35
      catch { case e: Throwable => log(e) }
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    36
    }
787ba47201c7 optional exception logging;
wenzelm
parents: 29191
diff changeset
    37
  }
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    38
}