src/Tools/Graphview/model.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 59259 399506ee38a5
permissions -rw-r--r--
more strict AFP properties;
     1 /*  Title:      Tools/Graphview/model.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 Internal graph representation.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.Color
    14 
    15 
    16 class Mutator_Container(val available: List[Mutator])
    17 {
    18   val events = new Mutator_Event.Bus
    19 
    20   private var _mutators : List[Mutator.Info] = Nil
    21   def apply() = _mutators
    22   def apply(mutators: List[Mutator.Info])
    23   {
    24     _mutators = mutators
    25     events.event(Mutator_Event.New_List(mutators))
    26   }
    27 
    28   def add(mutator: Mutator.Info)
    29   {
    30     _mutators = _mutators ::: List(mutator)
    31     events.event(Mutator_Event.Add(mutator))
    32   }
    33 }
    34 
    35 
    36 class Model(val full_graph: Graph_Display.Graph)
    37 {
    38   val Mutators =
    39     new Mutator_Container(
    40       List(
    41         Mutator.Node_Expression(".*", false, false, false),
    42         Mutator.Node_List(Nil, false, false, false),
    43         Mutator.Edge_Endpoints((Graph_Display.Node.dummy, Graph_Display.Node.dummy)),
    44         Mutator.Add_Node_Expression(""),
    45         Mutator.Add_Transitive_Closure(true, true)))
    46 
    47   val Colors =
    48     new Mutator_Container(
    49       List(
    50         Mutator.Node_Expression(".*", false, false, false),
    51         Mutator.Node_List(Nil, false, false, false)))
    52 
    53   def find_node(ident: String): Option[Graph_Display.Node] =
    54     full_graph.keys_iterator.find(node => node.ident == ident)
    55 
    56   def make_visible_graph(): Graph_Display.Graph =
    57     (full_graph /: Mutators()) {
    58       case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g)
    59     }
    60 
    61   private var _colors = Map.empty[Graph_Display.Node, Color]
    62   def colors = _colors
    63 
    64   private def build_colors()
    65   {
    66     _colors =
    67       (Map.empty[Graph_Display.Node, Color] /: Colors()) {
    68         case (colors, m) =>
    69           (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) {
    70             case (colors, node) => colors + (node -> m.color)
    71           }
    72       }
    73   }
    74   Colors.events += { case _ => build_colors() }
    75 }