# HG changeset patch
# User wenzelm
# Date 1420315625 -3600
# Node ID b12d76aa29fb7eb2013702047e952c720280f3c3
# Parent  abe4c7cdac0e4b50f97cabdb2168fe1c0c6b7700
tuned;

diff -r abe4c7cdac0e -r b12d76aa29fb src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:58:33 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 21:07:05 2015 +0100
@@ -56,24 +56,22 @@
   {
     private val identity = new AffineTransform()
 
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape =
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape =
     {
       val w = (m.space_width / 2).ceil
       new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
     }
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit =
-      paint_transformed(gfx, visualizer, node, identity)
+    def paint(gfx: Graphics2D, visualizer: Visualizer): Unit =
+      paint_transformed(gfx, visualizer, identity)
 
-    def paint_transformed(gfx: Graphics2D, visualizer: Visualizer,
-      node: Graph_Display.Node, at: AffineTransform)
+    def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
     {
       val m = Visualizer.Metrics(gfx)
-      val s = shape(m, visualizer, node)
-      val c = visualizer.node_color(node)
+      val s = shape(m, visualizer)
 
       gfx.setStroke(default_stroke)
-      gfx.setColor(c.border)
+      gfx.setColor(visualizer.dummy_color)
       gfx.draw(at.createTransformedShape(s))
     }
   }
@@ -101,7 +99,7 @@
         ds.foreach({
             case (x, y) => {
               val at = AffineTransform.getTranslateInstance(x, y)
-              Dummy.paint_transformed(gfx, visualizer, Graph_Display.Node.dummy, at)
+              Dummy.paint_transformed(gfx, visualizer, at)
             }
           })
       }
@@ -161,7 +159,7 @@
           ds.foreach({
               case (x, y) => {
                 val at = AffineTransform.getTranslateInstance(x, y)
-                Dummy.paint_transformed(gfx, visualizer, Graph_Display.Node.dummy, at)
+                Dummy.paint_transformed(gfx, visualizer, at)
               }
             })
         }
diff -r abe4c7cdac0e -r b12d76aa29fb src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 20:58:33 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 21:07:05 2015 +0100
@@ -54,10 +54,10 @@
   /* main colors */
 
   def foreground_color: Color = Color.BLACK
-  def foreground1_color: Color = Color.GRAY
   def background_color: Color = Color.WHITE
   def selection_color: Color = Color.GREEN
   def error_color: Color = Color.RED
+  def dummy_color: Color = Color.GRAY
 
 
   /* font rendering information */
@@ -199,7 +199,7 @@
     }
 
     def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
-      if (node.is_dummy) Shapes.Dummy.shape(m, visualizer, node)
+      if (node.is_dummy) Shapes.Dummy.shape(m, visualizer)
       else Shapes.Growing_Node.shape(m, visualizer, node)
   }
 
@@ -218,9 +218,7 @@
   sealed case class Node_Color(border: Color, background: Color, foreground: Color)
 
   def node_color(node: Graph_Display.Node): Node_Color =
-    if (node.is_dummy)
-      Node_Color(foreground1_color, background_color, foreground_color)
-    else if (Selection.contains(node))
+    if (Selection.contains(node))
       Node_Color(foreground_color, selection_color, foreground_color)
     else
       Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)