author | wenzelm |
Sun, 18 Jan 2015 19:21:10 +0100 | |
changeset 59395 | 4c5396f52546 |
parent 59392 | 02bacfc31446 |
child 59401 | 6ee01e011976 |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/visualizer.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 |
|
59395 | 5 |
Graph visualization parameters and GUI state. |
49557
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 |
|
50464 | 10 |
|
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49557
diff
changeset
|
11 |
import isabelle._ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
|
59290 | 13 |
import java.awt.{Font, Color, Shape, Graphics2D} |
59305 | 14 |
import java.awt.geom.{Point2D, Rectangle2D} |
49729 | 15 |
import javax.swing.JComponent |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
|
59395 | 18 |
abstract class Visualizer(val model: Model) |
50465 | 19 |
{ |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
20 |
visualizer => |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
21 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
22 |
|
59395 | 23 |
def options: Options |
59392 | 24 |
|
25 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
26 |
/* layout state */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
27 |
|
59290 | 28 |
// owned by GUI thread |
59303 | 29 |
private var _layout: Layout = Layout.empty |
30 |
def layout: Layout = _layout |
|
59290 | 31 |
|
32 |
def metrics: Metrics = layout.metrics |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
33 |
def visible_graph: Graph_Display.Graph = layout.input_graph |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
34 |
|
59303 | 35 |
def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit = |
36 |
_layout = _layout.translate_vertex(v, dx, dy) |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
37 |
|
59305 | 38 |
def find_node(at: Point2D): Option[Graph_Display.Node] = |
39 |
layout.output_graph.iterator.collectFirst({ |
|
59384 | 40 |
case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node |
59305 | 41 |
}) |
42 |
||
43 |
def find_dummy(at: Point2D): Option[Layout.Dummy] = |
|
44 |
layout.output_graph.iterator.collectFirst({ |
|
59384 | 45 |
case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy |
59305 | 46 |
}) |
47 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
48 |
def bounding_box(): Rectangle2D.Double = |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
49 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
50 |
var x0 = 0.0 |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
51 |
var y0 = 0.0 |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
52 |
var x1 = 0.0 |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
53 |
var y1 = 0.0 |
59384 | 54 |
for ((_, (info, _)) <- layout.output_graph.iterator) { |
55 |
val rect = Shapes.shape(info) |
|
56 |
x0 = x0 min rect.getMinX |
|
57 |
y0 = y0 min rect.getMinY |
|
58 |
x1 = x1 max rect.getMaxX |
|
59 |
y1 = y1 max rect.getMaxY |
|
60 |
} |
|
61 |
x0 = (x0 - metrics.gap).floor |
|
62 |
y0 = (y0 - metrics.gap).floor |
|
63 |
x1 = (x1 + metrics.gap).ceil |
|
64 |
y1 = (y1 + metrics.gap).ceil |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
65 |
new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
66 |
} |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
67 |
|
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
68 |
def update_layout() |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
69 |
{ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
70 |
val metrics = Metrics(make_font()) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
71 |
val visible_graph = model.make_visible_graph() |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
72 |
|
59384 | 73 |
def node_text(node: Graph_Display.Node, content: XML.Body): String = |
74 |
if (show_content) { |
|
75 |
val s = |
|
76 |
XML.content(Pretty.formatted( |
|
77 |
content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric)) |
|
78 |
if (s.nonEmpty) s else node.toString |
|
79 |
} |
|
80 |
else node.toString |
|
81 |
||
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
82 |
// FIXME avoid expensive operation on GUI thread |
59384 | 83 |
_layout = Layout.make(options, metrics, node_text _, visible_graph) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
84 |
} |
59290 | 85 |
|
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
86 |
|
59233 | 87 |
/* tooltips */ |
88 |
||
89 |
def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null |
|
90 |
||
91 |
||
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
92 |
/* main colors */ |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
93 |
|
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
94 |
def foreground_color: Color = Color.BLACK |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
95 |
def background_color: Color = Color.WHITE |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
96 |
def selection_color: Color = Color.GREEN |
59392 | 97 |
def current_color: Color = Color.YELLOW |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
98 |
def error_color: Color = Color.RED |
59251 | 99 |
def dummy_color: Color = Color.GRAY |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
100 |
|
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
101 |
|
50475 | 102 |
/* font rendering information */ |
103 |
||
59290 | 104 |
def make_font(): Font = |
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
105 |
{ |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
106 |
val family = options.string("graphview_font_family") |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
107 |
val size = options.int("graphview_font_size") |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
108 |
new Font(family, Font.PLAIN, size) |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
109 |
} |
50475 | 110 |
|
111 |
||
112 |
/* rendering parameters */ |
|
113 |
||
59294 | 114 |
// owned by GUI thread |
59384 | 115 |
var show_content = false |
116 |
var show_arrow_heads = false |
|
59294 | 117 |
var show_dummies = false |
50475 | 118 |
|
119 |
object Colors |
|
120 |
{ |
|
121 |
private val filter_colors = List( |
|
59220 | 122 |
new Color(0xD9, 0xF2, 0xE2), // blue |
123 |
new Color(0xFF, 0xE7, 0xD8), // orange |
|
124 |
new Color(0xFF, 0xFF, 0xE5), // yellow |
|
125 |
new Color(0xDE, 0xCE, 0xFF), // lilac |
|
126 |
new Color(0xCC, 0xEB, 0xFF), // turquoise |
|
127 |
new Color(0xFF, 0xE5, 0xE5), // red |
|
128 |
new Color(0xE5, 0xE5, 0xD9) // green |
|
50475 | 129 |
) |
130 |
||
131 |
private var curr : Int = -1 |
|
59220 | 132 |
def next(): Color = |
50475 | 133 |
{ |
134 |
curr = (curr + 1) % filter_colors.length |
|
135 |
filter_colors(curr) |
|
136 |
} |
|
137 |
} |
|
138 |
||
59294 | 139 |
def paint_all_visible(gfx: Graphics2D) |
140 |
{ |
|
141 |
gfx.setRenderingHints(Metrics.rendering_hints) |
|
142 |
for (edge <- visible_graph.edges_iterator) |
|
143 |
Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge) |
|
144 |
for (node <- visible_graph.keys_iterator) |
|
59384 | 145 |
Shapes.paint_node(gfx, visualizer, node) |
59294 | 146 |
} |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
147 |
|
59392 | 148 |
var alphabetic_order: Boolean = false |
149 |
var current_node: Option[Graph_Display.Node] = None |
|
150 |
||
50465 | 151 |
object Selection |
152 |
{ |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
153 |
// owned by GUI thread |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
154 |
private var state: List[Graph_Display.Node] = Nil |
50465 | 155 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
156 |
def get(): List[Graph_Display.Node] = GUI_Thread.require { state } |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
157 |
def contains(node: Graph_Display.Node): Boolean = get().contains(node) |
50465 | 158 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
159 |
def add(node: Graph_Display.Node): Unit = GUI_Thread.require { state = node :: state } |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
160 |
def clear(): Unit = GUI_Thread.require { state = Nil } |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
} |
50465 | 162 |
|
59220 | 163 |
sealed case class Node_Color(border: Color, background: Color, foreground: Color) |
50464 | 164 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
165 |
def node_color(node: Graph_Display.Node): Node_Color = |
59392 | 166 |
if (current_node == Some(node)) |
167 |
Node_Color(foreground_color, current_color, foreground_color) |
|
168 |
else if (Selection.contains(node)) |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
169 |
Node_Color(foreground_color, selection_color, foreground_color) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
170 |
else |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
171 |
Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color) |
59220 | 172 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
173 |
def edge_color(edge: Graph_Display.Edge): Color = foreground_color |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
} |