# HG changeset patch
# User wenzelm
# Date 1420374882 -3600
# Node ID d5c9900636eff2bac8c093a2abcce8ccaa420ef1
# Parent  a73d2b67897c69198852d18c938f2f4a916734d0
tuned signature;

diff -r a73d2b67897c -r d5c9900636ef src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 22:56:46 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sun Jan 04 13:34:42 2015 +0100
@@ -19,7 +19,7 @@
   private val default_stroke =
     new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-  object Growing_Node
+  object Node
   {
     def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
       : Rectangle2D.Double =
diff -r a73d2b67897c -r d5c9900636ef src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 22:56:46 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 04 13:34:42 2015 +0100
@@ -165,7 +165,7 @@
       var x1 = 0.0
       var y1 = 0.0
       for (node <- model.visible_nodes_iterator) {
-        val shape = Shapes.Growing_Node.shape(m, visualizer, node)
+        val shape = Shapes.Node.shape(m, visualizer, node)
         x0 = x0 min shape.getMinX
         y0 = y0 min shape.getMinY
         x1 = x1 max shape.getMaxX
@@ -182,7 +182,7 @@
   object Drawer
   {
     def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
-      if (!node.is_dummy) Shapes.Growing_Node.paint(gfx, visualizer, node)
+      if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
 
     def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
       Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
@@ -197,7 +197,7 @@
 
     def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
       if (node.is_dummy) Shapes.Dummy.shape(m, visualizer)
-      else Shapes.Growing_Node.shape(m, visualizer, node)
+      else Shapes.Node.shape(m, visualizer, node)
   }
 
   object Selection