# HG changeset patch
# User wenzelm
# Date 1420112055 -3600
# Node ID 261ec482cd406494eb3d6872d7a76d42bce0a57b
# Parent  6e77ddb1e3fb66c7a9b6b3f1960a53cbb63882da
tuned signature;

diff -r 6e77ddb1e3fb -r 261ec482cd40 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Thu Jan 01 12:20:22 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Thu Jan 01 12:34:15 2015 +0100
@@ -39,13 +39,13 @@
       val bounds = g.getFontMetrics.getStringBounds(caption, g)
       val s = shape(g, visualizer, peer)
 
-      val (border, background, foreground) = visualizer.Color(peer)
+      val c = visualizer.node_color(peer)
       g.setStroke(stroke)
-      g.setColor(border)
+      g.setColor(c.border)
       g.draw(s)
-      g.setColor(background)
+      g.setColor(c.background)
       g.fill(s)
-      g.setColor(foreground)
+      g.setColor(c.foreground)
       g.drawString(caption,
         (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
         (s.getCenterY + 5).toFloat)
@@ -67,9 +67,9 @@
     def paint_transformed(g: Graphics2D, visualizer: Visualizer,
       peer: Option[String], at: AffineTransform)
     {
-      val (border, background, foreground) = visualizer.Color(peer)
+      val c = visualizer.node_color(peer)
       g.setStroke(stroke)
-      g.setColor(border)
+      g.setColor(c.border)
       g.draw(at.createTransformedShape(shape))
     }
   }
@@ -111,7 +111,7 @@
       }
 
       g.setStroke(stroke)
-      g.setColor(visualizer.Color(peer))
+      g.setColor(visualizer.edge_color(peer))
       g.draw(path)
 
       if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
@@ -171,7 +171,7 @@
         }
 
         g.setStroke(stroke)
-        g.setColor(visualizer.Color(peer))
+        g.setColor(visualizer.edge_color(peer))
         g.draw(path)
 
         if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
diff -r 6e77ddb1e3fb -r 261ec482cd40 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Thu Jan 01 12:20:22 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Thu Jan 01 12:34:15 2015 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
+import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D}
 import java.awt.image.BufferedImage
 import javax.swing.JComponent
 
@@ -50,17 +50,17 @@
   object Colors
   {
     private val filter_colors = List(
-      new JColor(0xD9, 0xF2, 0xE2), // blue
-      new JColor(0xFF, 0xE7, 0xD8), // orange
-      new JColor(0xFF, 0xFF, 0xE5), // yellow
-      new JColor(0xDE, 0xCE, 0xFF), // lilac
-      new JColor(0xCC, 0xEB, 0xFF), // turquoise
-      new JColor(0xFF, 0xE5, 0xE5), // red
-      new JColor(0xE5, 0xE5, 0xD9)  // green
+      new Color(0xD9, 0xF2, 0xE2), // blue
+      new Color(0xFF, 0xE7, 0xD8), // orange
+      new Color(0xFF, 0xFF, 0xE5), // yellow
+      new Color(0xDE, 0xCE, 0xFF), // lilac
+      new Color(0xCC, 0xEB, 0xFF), // turquoise
+      new Color(0xFF, 0xE5, 0xE5), // red
+      new Color(0xE5, 0xE5, 0xD9)  // green
     )
 
     private var curr : Int = -1
-    def next(): JColor =
+    def next(): Color =
     {
       curr = (curr + 1) % filter_colors.length
       filter_colors(curr)
@@ -192,21 +192,17 @@
     def clear() { selected = Nil }
   }
 
-  object Color
-  {
-    def apply(l: Option[String]): (JColor, JColor, JColor) =
-      l match {
-        case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK)
-        case Some(c) => {
-            if (Selection(c))
-              (JColor.BLUE, JColor.GREEN, JColor.BLACK)
-            else
-              (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
-        }
-      }
+  sealed case class Node_Color(border: Color, background: Color, foreground: Color)
 
-    def apply(e: (String, String)): JColor = JColor.BLACK
-  }
+  def node_color(l: Option[String]): Node_Color =
+    l match {
+      case None => Node_Color(Color.GRAY, Color.WHITE, Color.BLACK)
+      case Some(c) =>
+        if (Selection(c)) Node_Color(Color.BLUE, Color.GREEN, Color.BLACK)
+        else Node_Color(Color.BLACK, model.colors.getOrElse(c, Color.WHITE), Color.BLACK)
+    }
+
+  def edge_color(e: (String, String)): Color = Color.BLACK
 
   object Caption
   {