author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73359 | d8a0e996614b |
child 78616 | 9acd819db33a |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/model.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 | 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 |
Internal graph representation. |
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 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
import isabelle._ |
55618 | 12 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
import java.awt.Color |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
75393 | 16 |
class Mutator_Container(val available: List[Mutator]) { |
59218 | 17 |
val events = new Mutator_Event.Bus |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
|
59221 | 19 |
private var _mutators : List[Mutator.Info] = Nil |
71601 | 20 |
def apply(): List[Mutator.Info] = _mutators |
75393 | 21 |
def apply(mutators: List[Mutator.Info]): Unit = { |
59218 | 22 |
_mutators = mutators |
59221 | 23 |
events.event(Mutator_Event.New_List(mutators)) |
59218 | 24 |
} |
25 |
||
75393 | 26 |
def add(mutator: Mutator.Info): Unit = { |
59218 | 27 |
_mutators = _mutators ::: List(mutator) |
28 |
events.event(Mutator_Event.Add(mutator)) |
|
29 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
30 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
31 |
|
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49557
diff
changeset
|
32 |
|
75393 | 33 |
class Model(val full_graph: Graph_Display.Graph) { |
59221 | 34 |
val Mutators = |
35 |
new Mutator_Container( |
|
36 |
List( |
|
37 |
Mutator.Node_Expression(".*", false, false, false), |
|
38 |
Mutator.Node_List(Nil, false, false, false), |
|
59246 | 39 |
Mutator.Edge_Endpoints((Graph_Display.Node.dummy, Graph_Display.Node.dummy)), |
59221 | 40 |
Mutator.Add_Node_Expression(""), |
41 |
Mutator.Add_Transitive_Closure(true, true))) |
|
59218 | 42 |
|
59221 | 43 |
val Colors = |
44 |
new Mutator_Container( |
|
45 |
List( |
|
46 |
Mutator.Node_Expression(".*", false, false, false), |
|
47 |
Mutator.Node_List(Nil, false, false, false))) |
|
59218 | 48 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
49 |
def find_node(ident: String): Option[Graph_Display.Node] = |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59246
diff
changeset
|
50 |
full_graph.keys_iterator.find(node => node.ident == ident) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
51 |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59246
diff
changeset
|
52 |
def make_visible_graph(): Graph_Display.Graph = |
73359 | 53 |
Mutators().foldLeft(full_graph) { |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59246
diff
changeset
|
54 |
case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g) |
59218 | 55 |
} |
56 |
||
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
57 |
private var _colors = Map.empty[Graph_Display.Node, Color] |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
58 |
def colors = _colors |
59218 | 59 |
|
75393 | 60 |
private def build_colors(): Unit = { |
59218 | 61 |
_colors = |
73359 | 62 |
Colors().foldLeft(Map.empty[Graph_Display.Node, Color]) { |
59221 | 63 |
case (colors, m) => |
73359 | 64 |
m.mutator.mutate(full_graph, full_graph).keys_iterator.foldLeft(colors) { |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
65 |
case (colors, node) => colors + (node -> m.color) |
59218 | 66 |
} |
67 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
68 |
} |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
69 |
Colors.events += { case _ => build_colors() } |
49854
c541bbad7024
store colors after build
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
49737
diff
changeset
|
70 |
} |