author | wenzelm |
Thu, 01 Jan 2015 20:50:20 +0100 | |
changeset 59231 | 6dea47cf6c6b |
parent 59228 | 56b34fc7a015 |
child 59233 | 876a81f5788b |
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 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
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
|
5 |
*/ |
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 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
|
55618 | 9 |
|
49558 | 10 |
import isabelle._ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
import java.awt.{Dimension, Graphics2D, Point, Rectangle} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
import java.awt.geom.{AffineTransform, Point2D} |
49732 | 14 |
import java.awt.image.BufferedImage |
59225 | 15 |
import javax.swing.{JScrollPane, JComponent, SwingUtilities} |
49729 | 16 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
import scala.swing.{Panel, ScrollPane} |
59225 | 18 |
import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged, |
19 |
MouseMoved, MouseClicked, MouseWheelMoved, 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 |
|
49731 | 22 |
class Graph_Panel( |
23 |
val visualizer: Visualizer, |
|
24 |
make_tooltip: (JComponent, Int, Int, XML.Body) => String) |
|
49729 | 25 |
extends ScrollPane |
26 |
{ |
|
49731 | 27 |
panel => |
49729 | 28 |
|
29 |
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { |
|
49730 | 30 |
override def getToolTipText(event: java.awt.event.MouseEvent): String = |
49732 | 31 |
node(Transform.pane_to_graph_coordinates(event.getPoint)) match { |
32 |
case Some(name) => |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59226
diff
changeset
|
33 |
visualizer.model.complete_graph.get_node(name).content match { |
49732 | 34 |
case Nil => null |
35 |
case content => make_tooltip(panel.peer, event.getX, event.getY, content) |
|
36 |
} |
|
37 |
case None => null |
|
38 |
} |
|
49729 | 39 |
} |
40 |
||
41 |
peer.setWheelScrollingEnabled(false) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
42 |
focusable = true |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
43 |
requestFocus() |
50470 | 44 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
45 |
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
|
46 |
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always |
49729 | 47 |
|
49732 | 48 |
def node(at: Point2D): Option[String] = |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
49 |
{ |
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
50 |
val gfx = visualizer.graphics_context() |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
51 |
visualizer.model.visible_nodes_iterator |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
52 |
.find(name => visualizer.Drawer.shape(gfx, Some(name)).contains(at)) |
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 |
|
57044 | 73 |
if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt) |
50478 | 74 |
refresh() |
75 |
} |
|
76 |
||
50470 | 77 |
def apply_layout() = visualizer.Coordinates.update_layout() |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
78 |
|
59218 | 79 |
private class Paint_Panel extends Panel |
80 |
{ |
|
81 |
def set_preferred_size() |
|
82 |
{ |
|
83 |
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() |
|
84 |
val s = Transform.scale_discrete |
|
85 |
val (px, py) = Transform.padding |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
86 |
|
59218 | 87 |
preferredSize = |
88 |
new Dimension( |
|
89 |
(math.abs(maxX - minX + px) * s).toInt, |
|
90 |
(math.abs(maxY - minY + py) * s).toInt) |
|
50470 | 91 |
|
59218 | 92 |
revalidate() |
93 |
} |
|
50470 | 94 |
|
59218 | 95 |
override def paint(g: Graphics2D) |
96 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
97 |
super.paintComponent(g) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
98 |
g.transform(Transform()) |
50470 | 99 |
|
49731 | 100 |
visualizer.Drawer.paint_all_visible(g, true) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
101 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
102 |
} |
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
|
103 |
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
|
104 |
contents = paint_panel |
50470 | 105 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
106 |
listenTo(keys) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
107 |
listenTo(mouse.moves) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
108 |
listenTo(mouse.clicks) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
109 |
listenTo(mouse.wheel) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
110 |
reactions += Interaction.Mouse.react |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
111 |
reactions += Interaction.Keyboard.react |
59218 | 112 |
reactions += |
113 |
{ |
|
114 |
case KeyTyped(_, _, _, _) => repaint(); requestFocus() |
|
115 |
case MousePressed(_, _, _, _, _) => repaint(); requestFocus() |
|
116 |
case MouseDragged(_, _, _) => repaint(); requestFocus() |
|
117 |
case MouseWheelMoved(_, _, _, _) => repaint(); requestFocus() |
|
118 |
case MouseClicked(_, _, _, _, _) => repaint(); requestFocus() |
|
119 |
case MouseMoved(_, _, _) => repaint() |
|
120 |
} |
|
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
121 |
|
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
122 |
visualizer.model.Colors.events += { case _ => repaint() } |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49732
diff
changeset
|
123 |
visualizer.model.Mutators.events += { case _ => repaint() } |
50470 | 124 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
125 |
apply_layout() |
50491 | 126 |
rescale(1.0) |
50470 | 127 |
|
50469 | 128 |
private object Transform |
129 |
{ |
|
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
130 |
val padding = (100, 40) |
50470 | 131 |
|
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
132 |
private var _scale: Double = 1.0 |
50477 | 133 |
def scale: Double = _scale |
134 |
def scale_=(s: Double) |
|
50468 | 135 |
{ |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
136 |
_scale = (s min 10) max 0.1 |
50468 | 137 |
} |
50477 | 138 |
def scale_discrete: Double = |
139 |
(_scale * visualizer.font_size).round.toDouble / visualizer.font_size |
|
50470 | 140 |
|
59218 | 141 |
def apply() = |
142 |
{ |
|
49731 | 143 |
val (minX, minY, _, _) = visualizer.Coordinates.bounds() |
50470 | 144 |
|
50477 | 145 |
val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
146 |
at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
147 |
at |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
148 |
} |
50470 | 149 |
|
59218 | 150 |
def fit_to_window() |
151 |
{ |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
152 |
if (visualizer.model.visible_nodes_iterator.isEmpty) |
50491 | 153 |
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
|
154 |
else { |
49731 | 155 |
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
156 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
157 |
val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2) |
49745 | 158 |
val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy) |
50491 | 159 |
rescale(sx min sy) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
} |
50470 | 162 |
|
59218 | 163 |
def pane_to_graph_coordinates(at: Point2D): Point2D = |
164 |
{ |
|
50477 | 165 |
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
|
166 |
val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null) |
50470 | 167 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
168 |
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
|
169 |
p |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
170 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
171 |
} |
50470 | 172 |
|
59218 | 173 |
object Interaction |
174 |
{ |
|
175 |
object Keyboard |
|
176 |
{ |
|
177 |
val react: PartialFunction[Event, Unit] = |
|
178 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
179 |
case KeyTyped(_, c, m, _) => typed(c, m) |
50470 | 180 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
181 |
|
59225 | 182 |
def typed(c: Char, m: Key.Modifiers) = |
59226 | 183 |
c match { |
184 |
case '+' => rescale(Transform.scale * 5.0/4) |
|
185 |
case '-' => rescale(Transform.scale * 4.0/5) |
|
186 |
case '0' => Transform.fit_to_window() |
|
187 |
case '1' => visualizer.Coordinates.update_layout() |
|
188 |
case '2' => Transform.fit_to_window() |
|
50470 | 189 |
case _ => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
190 |
} |
50470 | 191 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
192 |
|
59218 | 193 |
object Mouse |
194 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
195 |
type Dummy = ((String, String), Int) |
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 |
private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
198 |
|
59218 | 199 |
val react: PartialFunction[Event, Unit] = |
200 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
201 |
case MousePressed(_, p, _, _, _) => pressed(p) |
59218 | 202 |
case MouseDragged(_, to, _) => |
203 |
drag(draginfo, to) |
|
204 |
val (_, p, d) = draginfo |
|
205 |
draginfo = (to, p, d) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
206 |
case MouseWheelMoved(_, p, _, r) => wheel(r, p) |
59218 | 207 |
case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
208 |
} |
50470 | 209 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
def dummy(at: Point2D): Option[Dummy] = |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
211 |
{ |
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
212 |
val gfx = visualizer.graphics_context() |
59218 | 213 |
visualizer.model.visible_edges_iterator.map( |
214 |
i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({ |
|
50470 | 215 |
case (_, ((x, y), _)) => |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
216 |
visualizer.Drawer.shape(gfx, None).contains(at.getX() - x, at.getY() - y) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
217 |
}) match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
218 |
case None => None |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
219 |
case Some((name, (_, index))) => Some((name, index)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
220 |
} |
59231
6dea47cf6c6b
more dynamic visualizer -- re-use jEdit font info;
wenzelm
parents:
59228
diff
changeset
|
221 |
} |
50470 | 222 |
|
59218 | 223 |
def pressed(at: Point) |
224 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
225 |
val c = Transform.pane_to_graph_coordinates(at) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
226 |
val l = node(c) match { |
49731 | 227 |
case Some(l) => |
228 |
if (visualizer.Selection(l)) visualizer.Selection() else List(l) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
229 |
case None => Nil |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
230 |
} |
59218 | 231 |
val d = |
232 |
l match { |
|
233 |
case Nil => |
|
234 |
dummy(c) match { |
|
235 |
case Some(d) => List(d) |
|
236 |
case None => Nil |
|
237 |
} |
|
238 |
case _ => Nil |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
239 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
240 |
draginfo = (at, l, d) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
241 |
} |
50470 | 242 |
|
59225 | 243 |
def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent) |
59218 | 244 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
245 |
val c = Transform.pane_to_graph_coordinates(at) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
246 |
val p = node(c) |
50470 | 247 |
|
59218 | 248 |
def left_click() |
249 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
250 |
(p, m) match { |
59225 | 251 |
case (Some(l), Key.Modifier.Control) => visualizer.Selection.add(l) |
252 |
case (None, Key.Modifier.Control) => |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
253 |
|
59225 | 254 |
case (Some(l), Key.Modifier.Shift) => visualizer.Selection.add(l) |
255 |
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
|
256 |
|
49731 | 257 |
case (Some(l), _) => visualizer.Selection.set(List(l)) |
258 |
case (None, _) => visualizer.Selection.clear |
|
50470 | 259 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
260 |
} |
50470 | 261 |
|
59218 | 262 |
def right_click() |
263 |
{ |
|
49731 | 264 |
val menu = Popups(panel, p, visualizer.Selection()) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
265 |
menu.show(panel.peer, at.x, at.y) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
266 |
} |
50470 | 267 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
268 |
if (clicks < 2) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
269 |
if (SwingUtilities.isRightMouseButton(e.peer)) right_click() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
270 |
else left_click() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
271 |
} |
50470 | 272 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
273 |
|
59218 | 274 |
def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) |
275 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
276 |
val (from, p, d) = draginfo |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
277 |
|
50477 | 278 |
val s = Transform.scale_discrete |
50470 | 279 |
val (dx, dy) = (to.x - from.x, to.y - from.y) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
280 |
(p, d) match { |
59218 | 281 |
case (Nil, Nil) => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
282 |
val r = panel.peer.getViewport.getViewRect |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
283 |
r.translate(-dx, -dy) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
284 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
285 |
paint_panel.peer.scrollRectToVisible(r) |
50470 | 286 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
287 |
case (Nil, ds) => |
49731 | 288 |
ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s))) |
50470 | 289 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
290 |
case (ls, _) => |
49731 | 291 |
ls.foreach(l => visualizer.Coordinates.translate(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
|
292 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
293 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
294 |
|
59218 | 295 |
def wheel(rotation: Int, at: Point) |
296 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
297 |
val at2 = Transform.pane_to_graph_coordinates(at) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
298 |
// > 0 -> up |
50491 | 299 |
rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
300 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
301 |
// move mouseposition to center |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
302 |
Transform().transform(at2, at2) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
303 |
val r = panel.peer.getViewport.getViewRect |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
304 |
val (width, height) = (r.getWidth, r.getHeight) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
305 |
paint_panel.peer.scrollRectToVisible( |
59218 | 306 |
new Rectangle( |
307 |
(at2.getX() - width / 2).toInt, |
|
308 |
(at2.getY() - height / 2).toInt, |
|
309 |
width.toInt, |
|
310 |
height.toInt)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
311 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
312 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
313 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
314 |
} |