tuned signature;

--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:44:08 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:48:10 2015 +0100
@@ -16,13 +16,7 @@
 
 object Shapes
 {
-  trait Node
-  {
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape
-    def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit
-  }
-
-  object Growing_Node extends Node
+  object Growing_Node
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
@@ -58,7 +52,7 @@
     }
   }
 
-  object Dummy extends Node
+  object Dummy
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
@@ -86,13 +80,7 @@
     }
   }
 
-  trait Edge
-  {
-    def paint(g: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge,
-      head: Boolean, dummies: Boolean)
-  }
-
-  object Straight_Edge extends Edge
+  object Straight_Edge
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
@@ -132,7 +120,7 @@
     }
   }
 
-  object Cardinal_Spline_Edge extends Edge
+  object Cardinal_Spline_Edge
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)