author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
59459 | 1 |
/* Title: Tools/Graphview/graphview.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 |
|
59459 | 5 |
Graphview 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 |
|
75393 | 18 |
abstract class Graphview(full_graph: Graph_Display.Graph) { |
59459 | 19 |
graphview => |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
20 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
21 |
|
59395 | 22 |
def options: Options |
59392 | 23 |
|
59462 | 24 |
val model = new Model(full_graph) |
25 |
||
59392 | 26 |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
27 |
/* layout state */ |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
28 |
|
59290 | 29 |
// owned by GUI thread |
59303 | 30 |
private var _layout: Layout = Layout.empty |
31 |
def layout: Layout = _layout |
|
59290 | 32 |
|
33 |
def metrics: Metrics = layout.metrics |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
34 |
def visible_graph: Graph_Display.Graph = layout.input_graph |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
35 |
|
59303 | 36 |
def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit = |
37 |
_layout = _layout.translate_vertex(v, dx, dy) |
|
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
38 |
|
59305 | 39 |
def find_node(at: Point2D): Option[Graph_Display.Node] = |
40 |
layout.output_graph.iterator.collectFirst({ |
|
59384 | 41 |
case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node |
59305 | 42 |
}) |
43 |
||
44 |
def find_dummy(at: Point2D): Option[Layout.Dummy] = |
|
45 |
layout.output_graph.iterator.collectFirst({ |
|
59384 | 46 |
case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy |
59305 | 47 |
}) |
48 |
||
75393 | 49 |
def bounding_box(): Rectangle2D.Double = { |
59302
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 |
|
75393 | 68 |
def update_layout(): Unit = { |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
69 |
val metrics = Metrics(make_font()) |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
70 |
val visible_graph = model.make_visible_graph() |
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
71 |
|
59384 | 72 |
def node_text(node: Graph_Display.Node, content: XML.Body): String = |
73 |
if (show_content) { |
|
74 |
val s = |
|
67547
aefe7a7b330a
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
wenzelm
parents:
61590
diff
changeset
|
75 |
XML.content(Pretty.formatted(content, |
aefe7a7b330a
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
wenzelm
parents:
61590
diff
changeset
|
76 |
margin = options.int("graphview_content_margin").toDouble, |
aefe7a7b330a
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
wenzelm
parents:
61590
diff
changeset
|
77 |
metric = metrics.Pretty_Metric)) |
59384 | 78 |
if (s.nonEmpty) s else node.toString |
79 |
} |
|
80 |
else node.toString |
|
81 |
||
71601 | 82 |
_layout = Layout.make(options, metrics, node_text, visible_graph) |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
83 |
} |
59290 | 84 |
|
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
85 |
|
59233 | 86 |
/* tooltips */ |
87 |
||
88 |
def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null |
|
89 |
||
90 |
||
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
91 |
/* main colors */ |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
92 |
|
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
93 |
def foreground_color: Color = Color.BLACK |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
94 |
def background_color: Color = Color.WHITE |
61176 | 95 |
def selection_color: Color = new Color(204, 204, 255) |
96 |
def highlight_color: Color = new Color(255, 255, 224) |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
97 |
def error_color: Color = Color.RED |
59251 | 98 |
def dummy_color: Color = Color.GRAY |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
99 |
|
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59220
diff
changeset
|
100 |
|
50475 | 101 |
/* font rendering information */ |
102 |
||
75393 | 103 |
def make_font(): Font = { |
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
104 |
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
|
105 |
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
|
106 |
new Font(family, Font.PLAIN, size) |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59265
diff
changeset
|
107 |
} |
50475 | 108 |
|
109 |
||
110 |
/* rendering parameters */ |
|
111 |
||
59294 | 112 |
// owned by GUI thread |
59384 | 113 |
var show_content = false |
114 |
var show_arrow_heads = false |
|
59294 | 115 |
var show_dummies = false |
61176 | 116 |
var editor_style = false |
50475 | 117 |
|
75393 | 118 |
object Colors { |
50475 | 119 |
private val filter_colors = List( |
59220 | 120 |
new Color(0xD9, 0xF2, 0xE2), // blue |
121 |
new Color(0xFF, 0xE7, 0xD8), // orange |
|
122 |
new Color(0xFF, 0xFF, 0xE5), // yellow |
|
123 |
new Color(0xDE, 0xCE, 0xFF), // lilac |
|
124 |
new Color(0xCC, 0xEB, 0xFF), // turquoise |
|
125 |
new Color(0xFF, 0xE5, 0xE5), // red |
|
126 |
new Color(0xE5, 0xE5, 0xD9) // green |
|
50475 | 127 |
) |
128 |
||
129 |
private var curr : Int = -1 |
|
75393 | 130 |
def next(): Color = { |
50475 | 131 |
curr = (curr + 1) % filter_colors.length |
132 |
filter_colors(curr) |
|
133 |
} |
|
134 |
} |
|
135 |
||
75393 | 136 |
def paint(gfx: Graphics2D): Unit = { |
59294 | 137 |
gfx.setRenderingHints(Metrics.rendering_hints) |
59410 | 138 |
|
59459 | 139 |
for (node <- graphview.current_node) |
140 |
Shapes.highlight_node(gfx, graphview, node) |
|
59410 | 141 |
|
59294 | 142 |
for (edge <- visible_graph.edges_iterator) |
59459 | 143 |
Shapes.Cardinal_Spline_Edge.paint(gfx, graphview, edge) |
59410 | 144 |
|
59294 | 145 |
for (node <- visible_graph.keys_iterator) |
59459 | 146 |
Shapes.paint_node(gfx, graphview, node) |
59294 | 147 |
} |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
148 |
|
59392 | 149 |
var current_node: Option[Graph_Display.Node] = None |
150 |
||
75393 | 151 |
object Selection { |
61590 | 152 |
private val state = Synchronized[List[Graph_Display.Node]](Nil) |
50465 | 153 |
|
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59410
diff
changeset
|
154 |
def get(): List[Graph_Display.Node] = state.value |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
155 |
def contains(node: Graph_Display.Node): Boolean = get().contains(node) |
50465 | 156 |
|
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59410
diff
changeset
|
157 |
def add(node: Graph_Display.Node): Unit = state.change(node :: _) |
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59410
diff
changeset
|
158 |
def clear(): Unit = state.change(_ => Nil) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
159 |
} |
50465 | 160 |
|
59220 | 161 |
sealed case class Node_Color(border: Color, background: Color, foreground: Color) |
50464 | 162 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
163 |
def node_color(node: Graph_Display.Node): Node_Color = |
59410 | 164 |
if (Selection.contains(node)) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
165 |
Node_Color(foreground_color, selection_color, foreground_color) |
59410 | 166 |
else if (current_node == Some(node)) |
167 |
Node_Color(foreground_color, highlight_color, foreground_color) |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
168 |
else |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59242
diff
changeset
|
169 |
Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color) |
59220 | 170 |
|
59407 | 171 |
def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color = |
172 |
if (downwards || show_arrow_heads) foreground_color |
|
173 |
else error_color |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
} |