src/Tools/jEdit/src/utils/EventSource.scala
author wenzelm
Sun, 19 Oct 2008 16:51:55 +0200
changeset 34318 c13e168a8ae6
child 34407 aad6834ba380
permissions -rw-r--r--
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;

package isabelle.utils

import scala.collection.mutable.HashSet

class EventSource[Event] {
  private val handlers = new HashSet[(Event) => Unit]()

  def add(handler : (Event) => Unit) { handlers += handler }
  def remove(handler : (Event) => Unit) { handlers -= handler }
	
  def fire(event : Event) { for(h <- handlers) h(event) }
}