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;
     1 /*  Title:      Tools/Graphview/src/mutator_event.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3 
     4 Events for dialog synchronization.
     5 */
     6 
     7 package isabelle.graphview
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.collection.mutable
    13 
    14 import java.awt.Color
    15 
    16 
    17 object Mutator_Event
    18 {
    19   type Mutator_Markup = (Boolean, Color, Mutator)
    20 
    21   sealed abstract class Message
    22   case class Add(m: Mutator_Markup) extends Message
    23   case class NewList(m: List[Mutator_Markup]) extends Message
    24 
    25   type Receiver = PartialFunction[Message, Unit]
    26 
    27   class Bus
    28   {
    29     private val receivers = new mutable.ListBuffer[Receiver]
    30 
    31     def += (r: Receiver) { GUI_Thread.require {}; receivers += r }
    32     def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r }
    33     def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) }
    34   }
    35 }