src/Tools/Graphview/mutator_event.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 78615 abdf38ee314a
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59202
711c2446dc9d clarified source location;
wenzelm
parents: 57612
diff changeset
     1
/*  Title:      Tools/Graphview/mutator_event.scala
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     2
    Author:     Markus Kaiser, TU Muenchen
59240
e411afcfaa29 tuned headers;
wenzelm
parents: 59221
diff changeset
     3
    Author:     Makarius
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     4
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     5
Events for dialog synchronization.
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     6
*/
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     7
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     8
package isabelle.graphview
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     9
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    10
49733
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    11
import isabelle._
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    12
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    13
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    14
object Mutator_Event {
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    15
  sealed abstract class Message
59221
f779f83ef4ec tuned signature;
wenzelm
parents: 59202
diff changeset
    16
  case class Add(m: Mutator.Info) extends Message
f779f83ef4ec tuned signature;
wenzelm
parents: 59202
diff changeset
    17
  case class New_List(m: List[Mutator.Info]) extends Message
49733
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    18
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    19
  type Receiver = PartialFunction[Message, Unit]
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    20
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    21
  class Bus {
61590
wenzelm
parents: 59442
diff changeset
    22
    private val receivers = Synchronized[List[Receiver]](Nil)
49733
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    23
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 61590
diff changeset
    24
    def += (r: Receiver): Unit = receivers.change(Library.insert(r))
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 61590
diff changeset
    25
    def -= (r: Receiver): Unit = receivers.change(Library.remove(r))
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 61590
diff changeset
    26
    def event(x: Message): Unit = receivers.value.reverse.foreach(r => r(x))
49733
38a68e6593be prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents: 49565
diff changeset
    27
  }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    28
}