author | wenzelm |
Fri, 12 Aug 2022 11:47:12 +0200 | |
changeset 75810 | 51867c8ad109 |
parent 75809 | 1dd5d4f4b69e |
child 75839 | 29441f2bfe81 |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/graph_panel.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 |
|
59461 | 5 |
GUI panel for graph layout. |
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 |
|
55618 | 10 |
|
49558 | 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 |
|
59441 | 13 |
import java.awt.{Dimension, Graphics2D, Point, Rectangle} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
import java.awt.geom.{AffineTransform, Point2D} |
59408 | 15 |
import javax.imageio.ImageIO |
59225 | 16 |
import javax.swing.{JScrollPane, JComponent, SwingUtilities} |
59408 | 17 |
import javax.swing.border.EmptyBorder |
49729 | 18 |
|
59408 | 19 |
import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane} |
59253 | 20 |
import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
21 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
22 |
|
75393 | 23 |
class Graph_Panel(val graphview: Graphview) extends BorderPanel { |
59408 | 24 |
graph_panel => |
25 |
||
49729 | 26 |
|
59398 | 27 |
|
59408 | 28 |
/** graph **/ |
59398 | 29 |
|
59408 | 30 |
/* painter */ |
59243
21ef04bd4e17
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
wenzelm
parents:
59241
diff
changeset
|
31 |
|
75393 | 32 |
private val painter = new Panel { |
33 |
override def paint(gfx: Graphics2D): Unit = { |
|
59408 | 34 |
super.paintComponent(gfx) |
35 |
||
59459 | 36 |
gfx.setColor(graphview.background_color) |
59408 | 37 |
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight) |
38 |
||
39 |
gfx.transform(Transform()) |
|
59460 | 40 |
graphview.paint(gfx) |
59408 | 41 |
} |
49729 | 42 |
} |
43 |
||
75393 | 44 |
def set_preferred_size(): Unit = { |
59459 | 45 |
val box = graphview.bounding_box() |
59408 | 46 |
val s = Transform.scale_discrete |
47 |
painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt) |
|
48 |
painter.revalidate() |
|
49 |
} |
|
59398 | 50 |
|
75393 | 51 |
def refresh(): Unit = { |
59408 | 52 |
if (painter != null) { |
53 |
set_preferred_size() |
|
54 |
painter.repaint() |
|
55 |
} |
|
56 |
} |
|
59237
ac135eff1ffb
clarified mouse wheel: conventional scrolling, not scaling;
wenzelm
parents:
59234
diff
changeset
|
57 |
|
75393 | 58 |
def scroll_to_node(node: Graph_Display.Node): Unit = { |
59459 | 59 |
val gap = graphview.metrics.gap |
60 |
val info = graphview.layout.get_node(node) |
|
59398 | 61 |
|
62 |
val t = Transform() |
|
63 |
val p = |
|
64 |
t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null) |
|
65 |
val q = |
|
66 |
t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null) |
|
67 |
||
59408 | 68 |
painter.peer.scrollRectToVisible( |
59398 | 69 |
new Rectangle(p.getX.toInt, p.getY.toInt, |
70 |
(q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt)) |
|
49735
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
71 |
} |
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
72 |
|
50470 | 73 |
|
59408 | 74 |
/* scrollable graph pane */ |
75 |
||
76 |
private val graph_pane: ScrollPane = new ScrollPane(painter) { |
|
77 |
tooltip = "" |
|
50478 | 78 |
|
59408 | 79 |
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { |
80 |
override def getToolTipText(event: java.awt.event.MouseEvent): String = |
|
59459 | 81 |
graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { |
59408 | 82 |
case Some(node) => |
59459 | 83 |
graphview.model.full_graph.get_node(node) match { |
59408 | 84 |
case Nil => null |
85 |
case content => |
|
59459 | 86 |
graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content) |
59408 | 87 |
} |
88 |
case None => null |
|
89 |
} |
|
59218 | 90 |
} |
50470 | 91 |
|
59408 | 92 |
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always |
93 |
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always |
|
94 |
||
95 |
listenTo(mouse.moves) |
|
96 |
listenTo(mouse.clicks) |
|
97 |
reactions += |
|
75393 | 98 |
{ |
99 |
case MousePressed(_, p, _, _, _) => |
|
100 |
Mouse_Interaction.pressed(p) |
|
101 |
painter.repaint() |
|
102 |
case MouseDragged(_, to, _) => |
|
103 |
Mouse_Interaction.dragged(to) |
|
104 |
painter.repaint() |
|
105 |
case e @ MouseClicked(_, p, m, n, _) => |
|
106 |
Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer)) |
|
107 |
painter.repaint() |
|
108 |
} |
|
50470 | 109 |
|
59408 | 110 |
contents = painter |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
111 |
} |
59408 | 112 |
graph_pane.peer.getVerticalScrollBar.setUnitIncrement(10) |
50470 | 113 |
|
59408 | 114 |
|
115 |
/* transform */ |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
116 |
|
75393 | 117 |
def rescale(s: Double): Unit = { |
59398 | 118 |
Transform.scale = s |
119 |
if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt) |
|
120 |
refresh() |
|
121 |
} |
|
50470 | 122 |
|
75393 | 123 |
def fit_to_window(): Unit = { |
59399 | 124 |
Transform.fit_to_window() |
125 |
refresh() |
|
126 |
} |
|
127 |
||
75393 | 128 |
private object Transform { |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
129 |
private var _scale: Double = 1.0 |
50477 | 130 |
def scale: Double = _scale |
75393 | 131 |
def scale_=(s: Double): Unit = { |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
132 |
_scale = (s min 10.0) max 0.1 |
50468 | 133 |
} |
59255
db265648139c
clarified fit_to_window: floor scale within window bounds;
wenzelm
parents:
59253
diff
changeset
|
134 |
|
75393 | 135 |
def scale_discrete: Double = { |
59459 | 136 |
val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt |
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59262
diff
changeset
|
137 |
(scale * font_height).floor / font_height |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59262
diff
changeset
|
138 |
} |
50470 | 139 |
|
75393 | 140 |
def apply(): AffineTransform = { |
59459 | 141 |
val box = graphview.bounding_box() |
59397 | 142 |
val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) |
143 |
t.translate(- box.x, - box.y) |
|
144 |
t |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
145 |
} |
50470 | 146 |
|
75393 | 147 |
def fit_to_window(): Unit = { |
59459 | 148 |
if (graphview.visible_graph.is_empty) |
50491 | 149 |
rescale(1.0) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
150 |
else { |
59459 | 151 |
val box = graphview.bounding_box() |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
152 |
rescale((size.width / box.width) min (size.height / box.height)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
153 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
154 |
} |
50470 | 155 |
|
75393 | 156 |
def pane_to_graph_coordinates(at: Point2D): Point2D = { |
50477 | 157 |
val s = Transform.scale_discrete |
59408 | 158 |
val p = Transform().inverseTransform(graph_pane.peer.getViewport.getViewPosition, null) |
50470 | 159 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
p |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
162 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
163 |
} |
50470 | 164 |
|
59398 | 165 |
|
166 |
/* interaction */ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
167 |
|
59459 | 168 |
graphview.model.Colors.events += { case _ => painter.repaint() } |
169 |
graphview.model.Mutators.events += { case _ => painter.repaint() } |
|
59398 | 170 |
|
75393 | 171 |
private object Mouse_Interaction { |
59398 | 172 |
private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = |
173 |
(new Point(0, 0), Nil, Nil) |
|
59253 | 174 |
|
75393 | 175 |
def pressed(at: Point): Unit = { |
59253 | 176 |
val c = Transform.pane_to_graph_coordinates(at) |
177 |
val l = |
|
59459 | 178 |
graphview.find_node(c) match { |
59253 | 179 |
case Some(node) => |
59459 | 180 |
if (graphview.Selection.contains(node)) graphview.Selection.get() |
59253 | 181 |
else List(node) |
182 |
case None => Nil |
|
183 |
} |
|
184 |
val d = |
|
185 |
l match { |
|
59459 | 186 |
case Nil => graphview.find_dummy(c).toList |
59253 | 187 |
case _ => Nil |
188 |
} |
|
189 |
draginfo = (at, l, d) |
|
190 |
} |
|
50470 | 191 |
|
75393 | 192 |
def dragged(to: Point): Unit = { |
59398 | 193 |
val (from, p, d) = draginfo |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
194 |
|
59253 | 195 |
val s = Transform.scale_discrete |
59398 | 196 |
val dx = to.x - from.x |
197 |
val dy = to.y - from.y |
|
198 |
||
59253 | 199 |
(p, d) match { |
200 |
case (Nil, Nil) => |
|
59408 | 201 |
val r = graph_pane.peer.getViewport.getViewRect |
59302
4d985afc0565
explict layout graph structure, with dummies and coordinates;
wenzelm
parents:
59294
diff
changeset
|
202 |
r.translate(- dx, - dy) |
59408 | 203 |
painter.peer.scrollRectToVisible(r) |
50470 | 204 |
|
59253 | 205 |
case (Nil, ds) => |
59459 | 206 |
ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s)) |
59253 | 207 |
|
208 |
case (ls, _) => |
|
59459 | 209 |
ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
} |
59398 | 211 |
|
212 |
draginfo = (to, p, d) |
|
213 |
} |
|
214 |
||
75393 | 215 |
def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean): Unit = { |
59398 | 216 |
val c = Transform.pane_to_graph_coordinates(at) |
217 |
||
218 |
if (clicks < 2) { |
|
219 |
if (right_click) { |
|
59403 | 220 |
// FIXME |
221 |
if (false) { |
|
59459 | 222 |
val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get()) |
59408 | 223 |
menu.show(graph_pane.peer, at.x, at.y) |
59403 | 224 |
} |
59398 | 225 |
} |
226 |
else { |
|
59459 | 227 |
(graphview.find_node(c), m) match { |
228 |
case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node) |
|
59398 | 229 |
case (None, Key.Modifier.Control) => |
230 |
||
59459 | 231 |
case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node) |
59398 | 232 |
case (None, Key.Modifier.Shift) => |
233 |
||
234 |
case (Some(node), _) => |
|
59459 | 235 |
graphview.Selection.clear() |
236 |
graphview.Selection.add(node) |
|
59398 | 237 |
case (None, _) => |
59459 | 238 |
graphview.Selection.clear() |
59398 | 239 |
} |
240 |
} |
|
241 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
242 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
243 |
} |
59408 | 244 |
|
245 |
||
246 |
||
247 |
/** controls **/ |
|
248 |
||
249 |
private val mutator_dialog = |
|
59459 | 250 |
new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false) |
59408 | 251 |
private val color_dialog = |
59459 | 252 |
new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations") |
59408 | 253 |
|
254 |
private val chooser = new FileChooser { |
|
255 |
fileSelectionMode = FileChooser.SelectionMode.FilesOnly |
|
256 |
title = "Save image (.png or .pdf)" |
|
257 |
} |
|
258 |
||
59409 | 259 |
private val show_content = new CheckBox() { |
59459 | 260 |
selected = graphview.show_content |
59409 | 261 |
action = Action("Show content") { |
59459 | 262 |
graphview.show_content = selected |
263 |
graphview.update_layout() |
|
59409 | 264 |
refresh() |
265 |
} |
|
266 |
tooltip = "Show full node content within graph layout" |
|
267 |
} |
|
268 |
||
269 |
private val show_arrow_heads = new CheckBox() { |
|
59459 | 270 |
selected = graphview.show_arrow_heads |
59409 | 271 |
action = Action("Show arrow heads") { |
59459 | 272 |
graphview.show_arrow_heads = selected |
59409 | 273 |
painter.repaint() |
274 |
} |
|
275 |
tooltip = "Draw edges with explicit arrow heads" |
|
276 |
} |
|
277 |
||
278 |
private val show_dummies = new CheckBox() { |
|
59459 | 279 |
selected = graphview.show_dummies |
59409 | 280 |
action = Action("Show dummies") { |
59459 | 281 |
graphview.show_dummies = selected |
59409 | 282 |
painter.repaint() |
283 |
} |
|
284 |
tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging" |
|
285 |
} |
|
286 |
||
287 |
private val save_image = new Button { |
|
288 |
action = Action("Save image") { |
|
289 |
chooser.showSaveDialog(this) match { |
|
59441 | 290 |
case FileChooser.Result.Approve => |
59459 | 291 |
try { Graph_File.write(chooser.selectedFile, graphview) } |
59441 | 292 |
catch { |
293 |
case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) |
|
294 |
} |
|
59409 | 295 |
case _ => |
296 |
} |
|
297 |
} |
|
298 |
tooltip = "Save current graph layout as PNG or PDF" |
|
299 |
} |
|
300 |
||
75810 | 301 |
private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) } |
59409 | 302 |
|
303 |
private val fit_window = new Button { |
|
304 |
action = Action("Fit to window") { fit_to_window() } |
|
305 |
tooltip = "Zoom to fit window width and height" |
|
306 |
} |
|
307 |
||
308 |
private val update_layout = new Button { |
|
309 |
action = Action("Update layout") { |
|
59459 | 310 |
graphview.update_layout() |
59409 | 311 |
refresh() |
312 |
} |
|
313 |
tooltip = "Regenerate graph layout according to built-in algorithm" |
|
314 |
} |
|
315 |
||
61176 | 316 |
private val editor_style = new CheckBox() { |
317 |
selected = graphview.editor_style |
|
318 |
action = Action("Editor style") { |
|
319 |
graphview.editor_style = selected |
|
320 |
graphview.update_layout() |
|
321 |
refresh() |
|
322 |
} |
|
323 |
tooltip = "Use editor font and colors for painting" |
|
324 |
} |
|
325 |
||
73367 | 326 |
private val colorations = new Button { action = Action("Colorations") { color_dialog.open() } } |
327 |
private val filters = new Button { action = Action("Filters") { mutator_dialog.open() } } |
|
59409 | 328 |
|
59408 | 329 |
private val controls = |
66205 | 330 |
Wrap_Panel( |
331 |
List(show_content, show_arrow_heads, show_dummies, |
|
66206 | 332 |
save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters |
59408 | 333 |
|
334 |
||
335 |
||
336 |
/** main layout **/ |
|
337 |
||
338 |
layout(graph_pane) = BorderPanel.Position.Center |
|
339 |
layout(controls) = BorderPanel.Position.North |
|
340 |
||
341 |
rescale(1.0) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
342 |
} |