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