1/*  Title:      Tools/Graphview/model.scala
2    Author:     Markus Kaiser, TU Muenchen
3    Author:     Makarius
4
5Internal graph representation.
6*/
7
8package isabelle.graphview
9
10
11import isabelle._
12
13import java.awt.Color
14
15
16class 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
36class 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}
76