1 /* Title: Tools/Graphview/src/model.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Internal graph representation. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 import isabelle.graphview.Mutators._ |
|
12 |
|
13 import java.awt.Color |
|
14 |
|
15 |
|
16 class Mutator_Container(val available: List[Mutator]) { |
|
17 type Mutator_Markup = (Boolean, Color, Mutator) |
|
18 |
|
19 val events = new Mutator_Event.Bus |
|
20 |
|
21 private var _mutators : List[Mutator_Markup] = Nil |
|
22 def apply() = _mutators |
|
23 def apply(mutators: List[Mutator_Markup]){ |
|
24 _mutators = mutators |
|
25 |
|
26 events.event(Mutator_Event.NewList(mutators)) |
|
27 } |
|
28 |
|
29 def add(mutator: Mutator_Markup) = { |
|
30 _mutators = _mutators ::: List(mutator) |
|
31 |
|
32 events.event(Mutator_Event.Add(mutator)) |
|
33 } |
|
34 } |
|
35 |
|
36 |
|
37 object Model |
|
38 { |
|
39 /* node info */ |
|
40 |
|
41 sealed case class Info(name: String, content: XML.Body) |
|
42 |
|
43 val empty_info: Info = Info("", Nil) |
|
44 |
|
45 val decode_info: XML.Decode.T[Info] = (body: XML.Body) => |
|
46 { |
|
47 import XML.Decode._ |
|
48 |
|
49 val (name, content) = pair(string, x => x)(body) |
|
50 Info(name, content) |
|
51 } |
|
52 |
|
53 |
|
54 /* graph */ |
|
55 |
|
56 type Graph = isabelle.Graph[String, Info] |
|
57 |
|
58 val decode_graph: XML.Decode.T[Graph] = |
|
59 isabelle.Graph.decode(XML.Decode.string, decode_info) |
|
60 } |
|
61 |
|
62 class Model(private val graph: Model.Graph) { |
|
63 val Mutators = new Mutator_Container( |
|
64 List( |
|
65 Node_Expression(".*", false, false, false), |
|
66 Node_List(Nil, false, false, false), |
|
67 Edge_Endpoints("", ""), |
|
68 Add_Node_Expression(""), |
|
69 Add_Transitive_Closure(true, true) |
|
70 )) |
|
71 |
|
72 val Colors = new Mutator_Container( |
|
73 List( |
|
74 Node_Expression(".*", false, false, false), |
|
75 Node_List(Nil, false, false, false) |
|
76 )) |
|
77 |
|
78 def visible_nodes_iterator: Iterator[String] = current.keys_iterator |
|
79 |
|
80 def visible_edges_iterator: Iterator[(String, String)] = |
|
81 current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _))) |
|
82 |
|
83 def complete = graph |
|
84 def current: Model.Graph = |
|
85 (graph /: Mutators()) { |
|
86 case (g, (enabled, _, mutator)) => { |
|
87 if (!enabled) g |
|
88 else mutator.mutate(graph, g) |
|
89 } |
|
90 } |
|
91 |
|
92 private var _colors = Map.empty[String, Color] |
|
93 def colors = _colors |
|
94 |
|
95 private def build_colors() { |
|
96 _colors = |
|
97 (Map.empty[String, Color] /: Colors()) ({ |
|
98 case (colors, (enabled, color, mutator)) => { |
|
99 (colors /: mutator.mutate(graph, graph).keys_iterator) ({ |
|
100 case (colors, k) => colors + (k -> color) |
|
101 }) |
|
102 } |
|
103 }) |
|
104 } |
|
105 Colors.events += { case _ => build_colors() } |
|
106 } |
|