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