# HG changeset patch
# User wenzelm
# Date 1420560498 -3600
# Node ID b5e33012180ee9ef1e815987a52abd8a006ad77c
# Parent  848e27e4ac37ee9219e6740d022ab8c521260f79
tuned signature;

diff -r 848e27e4ac37 -r b5e33012180e src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:43:17 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 17:08:18 2015 +0100
@@ -26,7 +26,7 @@
 
   override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
-      find_visible_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+      visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
         case Some(node) =>
           visualizer.model.full_graph.get_node(node) match {
             case Nil => null
@@ -44,10 +44,6 @@
 
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
-  def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
-    visualizer.visible_graph.keys_iterator.find(node =>
-      Shapes.Node.shape(visualizer, node).contains(at))
-
   def refresh()
   {
     if (paint_panel != null) {
@@ -175,14 +171,11 @@
       case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
     }
 
-    def dummy(at: Point2D): Option[Layout.Dummy] =
-      visualizer.layout.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
-
     def pressed(at: Point)
     {
       val c = Transform.pane_to_graph_coordinates(at)
       val l =
-        find_visible_node(c) match {
+        visualizer.find_node(c) match {
           case Some(node) =>
             if (visualizer.Selection.contains(node)) visualizer.Selection.get()
             else List(node)
@@ -190,11 +183,7 @@
         }
       val d =
         l match {
-          case Nil =>
-            dummy(c) match {
-              case Some(d) => List(d)
-              case None => Nil
-            }
+          case Nil => visualizer.find_dummy(c).toList
           case _ => Nil
         }
       draginfo = (at, l, d)
@@ -206,7 +195,7 @@
 
       def left_click()
       {
-        (find_visible_node(c), m) match {
+        (visualizer.find_node(c), m) match {
           case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
           case (None, Key.Modifier.Control) =>
 
@@ -223,7 +212,7 @@
 
       def right_click()
       {
-        val menu = Popups(panel, find_visible_node(c), visualizer.Selection.get())
+        val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
         menu.show(panel.peer, at.x, at.y)
       }
 
diff -r 848e27e4ac37 -r b5e33012180e src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 16:43:17 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 17:08:18 2015 +0100
@@ -332,9 +332,6 @@
 
   /* dummies */
 
-  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
-    output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
-
   def dummies_iterator: Iterator[Layout.Point] =
     for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
 
diff -r 848e27e4ac37 -r b5e33012180e src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:43:17 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 17:08:18 2015 +0100
@@ -11,7 +11,7 @@
 import isabelle._
 
 import java.awt.{Font, Color, Shape, Graphics2D}
-import java.awt.geom.Rectangle2D
+import java.awt.geom.{Point2D, Rectangle2D}
 import javax.swing.JComponent
 
 
@@ -32,6 +32,16 @@
   def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
     _layout = _layout.translate_vertex(v, dx, dy)
 
+  def find_node(at: Point2D): Option[Graph_Display.Node] =
+    layout.output_graph.iterator.collectFirst({
+      case (Layout.Node(node), _) if Shapes.Node.shape(visualizer, node).contains(at) => node
+    })
+
+  def find_dummy(at: Point2D): Option[Layout.Dummy] =
+    layout.output_graph.iterator.collectFirst({
+      case (dummy: Layout.Dummy, (d, _)) if Shapes.Dummy.shape(visualizer, d).contains(at) => dummy
+    })
+
   def bounding_box(): Rectangle2D.Double =
   {
     var x0 = 0.0