# HG changeset patch
# User wenzelm
# Date 1420314670 -3600
# Node ID 50a3d663333af447fc0cc40ebdd1f18d33df2c61
# Parent  167c2ebdfab4907921366f427d2848ae5a22a447
tuned;

diff -r 167c2ebdfab4 -r 50a3d663333a src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:48:10 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:51:10 2015 +0100
@@ -16,11 +16,11 @@
 
 object Shapes
 {
+  private val default_stroke =
+    new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
   object Growing_Node
   {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-
     def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
       : Rectangle2D.Double =
     {
@@ -42,7 +42,7 @@
       g.fill(s)
 
       g.setColor(c.border)
-      g.setStroke(stroke)
+      g.setStroke(default_stroke)
       g.draw(s)
 
       g.setColor(c.foreground)
@@ -54,8 +54,6 @@
 
   object Dummy
   {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
     private val identity = new AffineTransform()
 
     def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape =
@@ -74,7 +72,7 @@
       val s = shape(m, visualizer, node)
       val c = visualizer.node_color(node)
 
-      g.setStroke(stroke)
+      g.setStroke(default_stroke)
       g.setColor(c.border)
       g.draw(at.createTransformedShape(s))
     }
@@ -82,9 +80,6 @@
 
   object Straight_Edge
   {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-
     def paint(g: Graphics2D, visualizer: Visualizer,
       edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
     {
@@ -111,7 +106,7 @@
           })
       }
 
-      g.setStroke(stroke)
+      g.setStroke(default_stroke)
       g.setColor(visualizer.edge_color(edge))
       g.draw(path)
 
@@ -122,8 +117,6 @@
 
   object Cardinal_Spline_Edge
   {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
     private val slack = 0.1
 
     def paint(g: Graphics2D, visualizer: Visualizer,
@@ -172,7 +165,7 @@
             })
         }
 
-        g.setStroke(stroke)
+        g.setStroke(default_stroke)
         g.setColor(visualizer.edge_color(edge))
         g.draw(path)