10 |
10 |
11 import isabelle._ |
11 import isabelle._ |
12 |
12 |
13 import java.awt.{Dimension, Graphics2D, Point} |
13 import java.awt.{Dimension, Graphics2D, Point} |
14 import java.awt.geom.{AffineTransform, Point2D} |
14 import java.awt.geom.{AffineTransform, Point2D} |
15 import java.awt.image.BufferedImage |
|
16 import javax.swing.{JScrollPane, JComponent, SwingUtilities} |
15 import javax.swing.{JScrollPane, JComponent, SwingUtilities} |
17 |
16 |
18 import scala.swing.{Panel, ScrollPane} |
17 import scala.swing.{Panel, ScrollPane} |
19 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent} |
18 import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent} |
20 |
19 |
44 verticalScrollBarPolicy = ScrollPane.BarPolicy.Always |
43 verticalScrollBarPolicy = ScrollPane.BarPolicy.Always |
45 |
44 |
46 peer.getVerticalScrollBar.setUnitIncrement(10) |
45 peer.getVerticalScrollBar.setUnitIncrement(10) |
47 |
46 |
48 def find_visible_node(at: Point2D): Option[Graph_Display.Node] = |
47 def find_visible_node(at: Point2D): Option[Graph_Display.Node] = |
49 { |
48 visualizer.visible_graph.keys_iterator.find(node => |
50 val m = visualizer.metrics() |
49 visualizer.Drawer.shape(node).contains(at)) |
51 visualizer.model.make_visible_graph().keys_iterator |
|
52 .find(node => visualizer.Drawer.shape(m, node).contains(at)) |
|
53 } |
|
54 |
50 |
55 def refresh() |
51 def refresh() |
56 { |
52 { |
57 if (paint_panel != null) { |
53 if (paint_panel != null) { |
58 paint_panel.set_preferred_size() |
54 paint_panel.set_preferred_size() |
179 case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) |
175 case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) |
180 } |
176 } |
181 |
177 |
182 def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] = |
178 def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] = |
183 { |
179 { |
184 val m = visualizer.metrics() |
180 visualizer.visible_graph.edges_iterator.map(edge => |
185 visualizer.model.make_visible_graph().edges_iterator.map( |
181 visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find( |
186 edge => |
182 { |
187 visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find( |
183 case (_, (p, _)) => |
188 { |
184 visualizer.Drawer.shape(Graph_Display.Node.dummy). |
189 case (_, (p, _)) => |
185 contains(at.getX() - p.x, at.getY() - p.y) |
190 visualizer.Drawer.shape(m, Graph_Display.Node.dummy). |
186 }) match { |
191 contains(at.getX() - p.x, at.getY() - p.y) |
187 case None => None |
192 }) match { |
188 case Some((edge, (_, index))) => Some((edge, index)) |
193 case None => None |
189 } |
194 case Some((edge, (_, index))) => Some((edge, index)) |
|
195 } |
|
196 } |
190 } |
197 |
191 |
198 def pressed(at: Point) |
192 def pressed(at: Point) |
199 { |
193 { |
200 val c = Transform.pane_to_graph_coordinates(at) |
194 val c = Transform.pane_to_graph_coordinates(at) |