# HG changeset patch
# User wenzelm
# Date 1420493378 -3600
# Node ID 506660c6792fb20fdb2414f4106a75686fd00b06
# Parent  569a8109eeb2f7579188fed7db6c46160198ceca
more direct coordinates for dummy;

diff -r 569a8109eeb2 -r 506660c6792f src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:47:12 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 22:29:38 2015 +0100
@@ -46,7 +46,7 @@
 
   def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
     visualizer.visible_graph.keys_iterator.find(node =>
-      visualizer.Drawer.shape(node).contains(at))
+      Shapes.Node.shape(visualizer, node).contains(at))
 
   def refresh()
   {
@@ -176,18 +176,12 @@
     }
 
     def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
-    {
       visualizer.visible_graph.edges_iterator.map(edge =>
-        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
-          {
-            case (_, (p, _)) =>
-              visualizer.Drawer.shape(Graph_Display.Node.dummy).
-                contains(at.getX() - p.x, at.getY() - p.y)
-          }) match {
-            case None => None
-            case Some((edge, (_, index))) => Some((edge, index))
-          }
-    }
+        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.
+          collectFirst({
+            case (edge, (d, index))
+            if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index)
+          })
 
     def pressed(at: Point)
     {
diff -r 569a8109eeb2 -r 506660c6792f src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 21:47:12 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 22:29:38 2015 +0100
@@ -55,23 +55,18 @@
 
   object Dummy
   {
-    private val identity = new AffineTransform()
-
-    def shape(visualizer: Visualizer): Shape =
+    def shape(visualizer: Visualizer, d: Layout.Point): Shape =
     {
-      val m = visualizer.metrics
-      val w = (m.space_width / 2).ceil
-      new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
+      val metrics = visualizer.metrics
+      val w = metrics.space_width
+      new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
     }
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer): Unit =
-      paint_transformed(gfx, visualizer, identity)
-
-    def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
     {
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.dummy_color)
-      gfx.draw(at.createTransformedShape(shape(visualizer)))
+      gfx.draw(shape(visualizer, d))
     }
   }
 
@@ -94,15 +89,13 @@
       ds.foreach(d => path.lineTo(d.x, d.y))
       path.lineTo(q.x, q.y)
 
-      if (dummies)
-        ds.foreach(d =>
-          Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+      if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
 
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.edge_color(edge))
       gfx.draw(path)
 
-      if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
+      if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
     }
   }
 
@@ -149,15 +142,13 @@
           q.x - slack * dx2, q.y - slack * dy2,
           q.x, q.y)
 
-        if (dummies)
-          ds.foreach(d =>
-            Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+        if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
 
         gfx.setStroke(default_stroke)
         gfx.setColor(visualizer.edge_color(edge))
         gfx.draw(path)
 
-        if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
+        if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
       }
     }
   }
diff -r 569a8109eeb2 -r 506660c6792f src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 21:47:12 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 22:29:38 2015 +0100
@@ -142,10 +142,6 @@
       visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
       visible_graph.keys_iterator.foreach(apply(gfx, _))
     }
-
-    def shape(node: Graph_Display.Node): Shape =
-      if (node.is_dummy) Shapes.Dummy.shape(visualizer)
-      else Shapes.Node.shape(visualizer, node)
   }
 
   object Selection