# HG changeset patch
# User wenzelm
# Date 1355157857 -3600
# Node ID 37b53813426f342fb4d37ee912016e2232c90531
# Parent  1d7e506a3a77b13e52acdc579852f17560345224
tuned signature;

diff -r 1d7e506a3a77 -r 37b53813426f src/Tools/Graphview/src/shapes.scala
--- a/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 17:05:51 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala	Mon Dec 10 17:44:17 2012 +0100
@@ -21,7 +21,7 @@
     private val stroke =
       new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) = {
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double = {
       val caption = visualizer.Caption(peer.get)
       val bounds = g.getFontMetrics.getStringBounds(caption, g)
       val (x, y) = visualizer.Coordinates(peer.get)
@@ -59,13 +59,14 @@
     private val shape = new Rectangle2D.Double(-8, -8, 16, 16)
     private val identity = new AffineTransform()
 
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) = shape
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape
 
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) =
+    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
       paint_transformed(g, visualizer, peer, identity)
     
     def paint_transformed(g: Graphics2D, visualizer: Visualizer,
-                          peer: Option[String], at: AffineTransform) = {
+                          peer: Option[String], at: AffineTransform)
+    {
       val (border, background, foreground) = visualizer.Color(peer)
       g.setStroke(stroke)
       g.setColor(border)
@@ -83,7 +84,8 @@
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-              peer: (String, String), head: Boolean, dummies: Boolean) {
+              peer: (String, String), head: Boolean, dummies: Boolean)
+    {
       val ((fx, fy), (tx, ty)) =
         (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
       val ds = {
@@ -120,7 +122,8 @@
     private val slack = 0.1
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-              peer: (String, String), head: Boolean, dummies: Boolean) {
+              peer: (String, String), head: Boolean, dummies: Boolean)
+    {
       val ((fx, fy), (tx, ty)) =
         (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
       val ds = {
@@ -230,7 +233,8 @@
       }
     }
     
-    def paint(g: Graphics2D, path: GeneralPath, shape: Shape) {
+    def paint(g: Graphics2D, path: GeneralPath, shape: Shape)
+    {
       position(path, shape) match {
         case None =>
         case Some(at) => {
diff -r 1d7e506a3a77 -r 37b53813426f src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 17:05:51 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 17:44:17 2012 +0100
@@ -6,8 +6,11 @@
 
 package isabelle.graphview
 
+
 import isabelle._
 
+
+import java.awt.{Font => JFont, Color => JColor, Shape}
 import java.awt.{RenderingHints, Graphics2D}
 import javax.swing.JComponent
 
@@ -76,9 +79,9 @@
   }
   
   private val visualizer = this
-  object Drawer {
+  object Drawer
+  {
     import Shapes._
-    import java.awt.Shape
     
     def apply(g: Graphics2D, n: Option[String]) = n match {
       case None => 
@@ -89,8 +92,10 @@
       Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
     }
     
-    def paint_all_visible(g: Graphics2D, dummies: Boolean) = {
+    def paint_all_visible(g: Graphics2D, dummies: Boolean)
+    {
       g.setFont(Font())
+
       g.setRenderingHints(rendering_hints)
 
       model.visible_edges().foreach(e => {
@@ -119,35 +124,33 @@
     def clear() { selected = Nil }
   }
   
-  object Color {
-    import java.awt.{Color => awtColor}
-    
-    def apply(l: Option[String]): (awtColor, awtColor, awtColor) = l match {
-      case None => (awtColor.GRAY, awtColor.WHITE, awtColor.BLACK)
+  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))
-            (awtColor.BLUE, awtColor.GREEN, awtColor.BLACK)
+            (JColor.BLUE, JColor.GREEN, JColor.BLACK)
           else
-            (awtColor.BLACK,
-             model.colors.getOrElse(c, awtColor.WHITE), awtColor.BLACK)
+            (JColor.BLACK,
+             model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
       }
     }
       
-    def apply(e: (String, String)): awtColor = awtColor.BLACK
+    def apply(e: (String, String)): JColor = JColor.BLACK
   }  
+
+  object Font
+  {
+    def apply(): JFont =
+      new JFont(Parameters.font_family, JFont.BOLD, Parameters.font_size)
+  }
   
   object Caption {    
     def apply(key: String) =
       if (Parameters.long_names) key
       else model.complete.get_node(key).name
   }
-  
-  object Font {
-    import java.awt.{Font => awtFont}
-    
-    def apply() = new awtFont(Parameters.font_family,
-                              awtFont.BOLD, Parameters.font_size)
-  }
 
   val rendering_hints =
     new RenderingHints(