author | wenzelm |
Mon, 05 Jan 2015 14:13:38 +0100 | |
changeset 59286 | ac74eedb910a |
parent 59262 | 5cd92c743958 |
child 59287 | 9d4728e00925 |
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 |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
13 |
import java.awt.{Dimension, Graphics2D, Point} |
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} |
49732 | 15 |
import java.awt.image.BufferedImage |
59225 | 16 |
import javax.swing.{JScrollPane, JComponent, SwingUtilities} |
49729 | 17 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
import scala.swing.{Panel, ScrollPane} |
59253 | 19 |
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
|
20 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
21 |
|
59233 | 22 |
class Graph_Panel(val visualizer: Visualizer) extends ScrollPane |
49729 | 23 |
{ |
49731 | 24 |
panel => |
49729 | 25 |
|
59243
21ef04bd4e17
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
wenzelm
parents:
59241
diff
changeset
|
26 |
tooltip = "" |
21ef04bd4e17
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
wenzelm
parents:
59241
diff
changeset
|
27 |
|
49729 | 28 |
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { |
49730 | 29 |
override def getToolTipText(event: java.awt.event.MouseEvent): String = |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
30 |
find_visible_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59243
diff
changeset
|
31 |
case Some(node) => |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
32 |
visualizer.model.full_graph.get_node(node) match { |
49732 | 33 |
case Nil => null |
59233 | 34 |
case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content) |
49732 | 35 |
} |
36 |
case None => null |
|
37 |
} |
|
49729 | 38 |
} |
39 |
||
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
40 |
focusable = true |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
41 |
requestFocus() |
50470 | 42 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
43 |
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
44 |
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always |
49729 | 45 |
|
59237
ac135eff1ffb
clarified mouse wheel: conventional scrolling, not scaling;
wenzelm
parents:
59234
diff
changeset
|
46 |
peer.getVerticalScrollBar.setUnitIncrement(10) |
ac135eff1ffb
clarified mouse wheel: conventional scrolling, not scaling;
wenzelm
parents:
59234
diff
changeset
|
47 |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
48 |
def find_visible_node(at: Point2D): Option[Graph_Display.Node] = |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
49 |
{ |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
50 |
val m = visualizer.metrics() |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
51 |
visualizer.model.make_visible_graph().keys_iterator |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59243
diff
changeset
|
52 |
.find(node => visualizer.Drawer.shape(m, node).contains(at)) |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
53 |
} |
49732 | 54 |
|
49735
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
55 |
def refresh() |
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
56 |
{ |
50491 | 57 |
if (paint_panel != null) { |
58 |
paint_panel.set_preferred_size() |
|
59 |
paint_panel.repaint() |
|
60 |
} |
|
49735
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
61 |
} |
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
62 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
63 |
def fit_to_window() = { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
64 |
Transform.fit_to_window() |
49735
30e2f3f1c623
more precise repaint and revalidate -- the latter is important to keep in sync with content update;
wenzelm
parents:
49733
diff
changeset
|
65 |
refresh() |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
66 |
} |
50470 | 67 |
|
57044 | 68 |
val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } |
50491 | 69 |
|
50478 | 70 |
def rescale(s: Double) |
71 |
{ |
|
72 |
Transform.scale = s |
|
59255
db265648139c
clarified fit_to_window: floor scale within window bounds;
wenzelm
parents:
59253
diff
changeset
|
73 |
if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt) |
50478 | 74 |
refresh() |
75 |
} |
|
76 |
||
59253 | 77 |
def apply_layout() |
78 |
{ |
|
79 |
visualizer.Coordinates.update_layout() |
|
80 |
repaint() |
|
81 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
82 |
|
59218 | 83 |
private class Paint_Panel extends Panel |
84 |
{ |
|
85 |
def set_preferred_size() |
|
86 |
{ |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
87 |
val box = visualizer.Coordinates.bounding_box() |
59218 | 88 |
val s = Transform.scale_discrete |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
89 |
|
59218 | 90 |
preferredSize = |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
91 |
new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt) |
50470 | 92 |
|
59218 | 93 |
revalidate() |
94 |
} |
|
50470 | 95 |
|
59250 | 96 |
override def paint(gfx: Graphics2D) |
59218 | 97 |
{ |
59250 | 98 |
super.paintComponent(gfx) |
99 |
gfx.setColor(visualizer.background_color) |
|
100 |
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight) |
|
101 |
gfx.transform(Transform()) |
|
50470 | 102 |
|
59250 | 103 |
visualizer.Drawer.paint_all_visible(gfx, true) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
104 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
105 |
} |
49954
44658062d822
more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
wenzelm
parents:
49745
diff
changeset
|
106 |
private val paint_panel = new Paint_Panel |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
107 |
contents = paint_panel |
50470 | 108 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
109 |
listenTo(mouse.moves) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
110 |
listenTo(mouse.clicks) |
59253 | 111 |
reactions += Mouse_Interaction.react |
59218 | 112 |
reactions += |
113 |
{ |
|
59253 | 114 |
case MousePressed(_, _, _, _, _) => repaint() |
115 |
case MouseDragged(_, _, _) => repaint() |
|
116 |
case MouseClicked(_, _, _, _, _) => repaint() |
|
59218 | 117 |
} |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
118 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
119 |
visualizer.model.Colors.events += { case _ => repaint() } |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
120 |
visualizer.model.Mutators.events += { case _ => repaint() } |
50470 | 121 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
122 |
apply_layout() |
50491 | 123 |
rescale(1.0) |
50470 | 124 |
|
50469 | 125 |
private object Transform |
126 |
{ |
|
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
127 |
private var _scale: Double = 1.0 |
50477 | 128 |
def scale: Double = _scale |
129 |
def scale_=(s: Double) |
|
50468 | 130 |
{ |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
131 |
_scale = (s min 10.0) max 0.1 |
50468 | 132 |
} |
59255
db265648139c
clarified fit_to_window: floor scale within window bounds;
wenzelm
parents:
59253
diff
changeset
|
133 |
|
50477 | 134 |
def scale_discrete: Double = |
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59262
diff
changeset
|
135 |
{ |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59262
diff
changeset
|
136 |
val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble |
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 |
|
59218 | 140 |
def apply() = |
141 |
{ |
|
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
142 |
val box = visualizer.Coordinates.bounding_box() |
50477 | 143 |
val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
144 |
at.translate(- box.x, - box.y) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
145 |
at |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
146 |
} |
50470 | 147 |
|
59218 | 148 |
def fit_to_window() |
149 |
{ |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
150 |
if (visualizer.model.make_visible_graph().is_empty) |
50491 | 151 |
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
|
152 |
else { |
59241
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
153 |
val box = visualizer.Coordinates.bounding_box() |
541b95e94dc7
clarified bounding box, similar to old graph browser;
wenzelm
parents:
59240
diff
changeset
|
154 |
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
|
155 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
156 |
} |
50470 | 157 |
|
59218 | 158 |
def pane_to_graph_coordinates(at: Point2D): Point2D = |
159 |
{ |
|
50477 | 160 |
val s = Transform.scale_discrete |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null) |
50470 | 162 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
163 |
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
|
164 |
p |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
165 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
166 |
} |
50470 | 167 |
|
59253 | 168 |
object Mouse_Interaction |
59218 | 169 |
{ |
59262 | 170 |
private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
171 |
|
59253 | 172 |
val react: PartialFunction[Event, Unit] = |
173 |
{ |
|
174 |
case MousePressed(_, p, _, _, _) => pressed(p) |
|
175 |
case MouseDragged(_, to, _) => |
|
176 |
drag(draginfo, to) |
|
177 |
val (_, p, d) = draginfo |
|
178 |
draginfo = (to, p, d) |
|
179 |
case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) |
|
180 |
} |
|
181 |
||
59262 | 182 |
def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] = |
59253 | 183 |
{ |
184 |
val m = visualizer.metrics() |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
185 |
visualizer.model.make_visible_graph().edges_iterator.map( |
59262 | 186 |
edge => |
187 |
visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find( |
|
188 |
{ |
|
189 |
case (_, (p, _)) => |
|
190 |
visualizer.Drawer.shape(m, Graph_Display.Node.dummy). |
|
191 |
contains(at.getX() - p.x, at.getY() - p.y) |
|
192 |
}) match { |
|
193 |
case None => None |
|
194 |
case Some((edge, (_, index))) => Some((edge, index)) |
|
195 |
} |
|
50470 | 196 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
197 |
|
59253 | 198 |
def pressed(at: Point) |
59218 | 199 |
{ |
59253 | 200 |
val c = Transform.pane_to_graph_coordinates(at) |
201 |
val l = |
|
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
202 |
find_visible_node(c) match { |
59253 | 203 |
case Some(node) => |
204 |
if (visualizer.Selection.contains(node)) visualizer.Selection.get() |
|
205 |
else List(node) |
|
206 |
case None => Nil |
|
207 |
} |
|
208 |
val d = |
|
209 |
l match { |
|
210 |
case Nil => |
|
211 |
dummy(c) match { |
|
212 |
case Some(d) => List(d) |
|
213 |
case None => Nil |
|
214 |
} |
|
215 |
case _ => Nil |
|
216 |
} |
|
217 |
draginfo = (at, l, d) |
|
218 |
} |
|
50470 | 219 |
|
59253 | 220 |
def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent) |
221 |
{ |
|
222 |
val c = Transform.pane_to_graph_coordinates(at) |
|
50470 | 223 |
|
59253 | 224 |
def left_click() |
59218 | 225 |
{ |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
226 |
(find_visible_node(c), m) match { |
59253 | 227 |
case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node) |
228 |
case (None, Key.Modifier.Control) => |
|
50470 | 229 |
|
59253 | 230 |
case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node) |
231 |
case (None, Key.Modifier.Shift) => |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
232 |
|
59253 | 233 |
case (Some(node), _) => |
234 |
visualizer.Selection.clear() |
|
235 |
visualizer.Selection.add(node) |
|
236 |
case (None, _) => |
|
237 |
visualizer.Selection.clear() |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
238 |
} |
50470 | 239 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
240 |
|
59253 | 241 |
def right_click() |
59218 | 242 |
{ |
59259
399506ee38a5
clarified static full_graph vs. dynamic visible_graph;
wenzelm
parents:
59255
diff
changeset
|
243 |
val menu = Popups(panel, find_visible_node(c), visualizer.Selection.get()) |
59253 | 244 |
menu.show(panel.peer, at.x, at.y) |
245 |
} |
|
246 |
||
247 |
if (clicks < 2) { |
|
248 |
if (SwingUtilities.isRightMouseButton(e.peer)) right_click() |
|
249 |
else left_click() |
|
250 |
} |
|
251 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
252 |
|
59262 | 253 |
def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point) |
59253 | 254 |
{ |
59262 | 255 |
val (from, p, d) = info |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
256 |
|
59253 | 257 |
val s = Transform.scale_discrete |
258 |
val (dx, dy) = (to.x - from.x, to.y - from.y) |
|
259 |
(p, d) match { |
|
260 |
case (Nil, Nil) => |
|
261 |
val r = panel.peer.getViewport.getViewRect |
|
262 |
r.translate(-dx, -dy) |
|
50470 | 263 |
|
59253 | 264 |
paint_panel.peer.scrollRectToVisible(r) |
50470 | 265 |
|
59253 | 266 |
case (Nil, ds) => |
59262 | 267 |
ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s)) |
59253 | 268 |
|
269 |
case (ls, _) => |
|
59262 | 270 |
ls.foreach(l => visualizer.Coordinates.translate_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
|
271 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
272 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
273 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
274 |
} |