src/Pure/General/event_bus.scala
author wenzelm
Mon, 29 Dec 2008 15:13:53 +0100
changeset 29191 de56edf88514
parent 29190 89217ccfd130
child 29200 787ba47201c7
permissions -rw-r--r--
added methods "+" and "-"; event: non-synchronized execution of handlers, based on synchronized snapshot;
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
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     4
Generic event bus.
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     5
*/
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     6
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     7
package isabelle
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
     8
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
     9
import scala.collection.mutable.ListBuffer
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    10
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    11
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    12
class EventBus[Event] {
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    13
  type Handler = Event => Unit
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    14
  private val handlers = new ListBuffer[Handler]
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    15
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    16
  def += (h: Handler) = synchronized { handlers += h }
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    17
  def + (h: Handler) = { this += h; this }
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    18
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    19
  def -= (h: Handler) = synchronized { handlers -= h }
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    20
  def - (h: Handler) = { this -= h; this }
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    21
29191
de56edf88514 added methods "+" and "-";
wenzelm
parents: 29190
diff changeset
    22
  def event(e: Event) = synchronized { handlers.toList } foreach (h => h(e))
29190
89217ccfd130 Generic event bus.
wenzelm
parents:
diff changeset
    23
}