src/Tools/Graphview/src/mutator_event.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
markus@49557
     1
/*  Title:      Tools/Graphview/src/mutator_event.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
markus@49557
     3
markus@49557
     4
Events for dialog synchronization.
markus@49557
     5
*/
markus@49557
     6
markus@49557
     7
package isabelle.graphview
markus@49557
     8
markus@49557
     9
wenzelm@49733
    10
import isabelle._
wenzelm@49733
    11
wenzelm@49733
    12
import scala.collection.mutable
wenzelm@49733
    13
markus@49557
    14
import java.awt.Color
markus@49557
    15
markus@49557
    16
markus@49557
    17
object Mutator_Event
markus@49557
    18
{
wenzelm@49565
    19
  type Mutator_Markup = (Boolean, Color, Mutator)
wenzelm@49733
    20
markus@49557
    21
  sealed abstract class Message
markus@49557
    22
  case class Add(m: Mutator_Markup) extends Message
markus@49557
    23
  case class NewList(m: List[Mutator_Markup]) extends Message
wenzelm@49733
    24
wenzelm@49733
    25
  type Receiver = PartialFunction[Message, Unit]
wenzelm@49733
    26
wenzelm@49733
    27
  class Bus
wenzelm@49733
    28
  {
wenzelm@49733
    29
    private val receivers = new mutable.ListBuffer[Receiver]
wenzelm@49733
    30
wenzelm@57612
    31
    def += (r: Receiver) { GUI_Thread.require {}; receivers += r }
wenzelm@57612
    32
    def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r }
wenzelm@57612
    33
    def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) }
wenzelm@49733
    34
  }
markus@49557
    35
}