# HG changeset patch
# User wenzelm
# Date 1420314490 -3600
# Node ID 167c2ebdfab4907921366f427d2848ae5a22a447
# Parent  67bb4b3e150452a588a65f5da75a798c82f7d5f0
tuned signature;

diff -r 67bb4b3e1504 -r 167c2ebdfab4 src/Tools/Graphview/shapes.scala
--- 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)