clarified metrics, similar to old graph browser;

--- a/src/Tools/Graphview/shapes.scala	Thu Jan 01 21:23:01 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Fri Jan 02 19:54:13 2015 +0100
@@ -27,17 +27,19 @@
     def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
     {
       val (x, y) = visualizer.Coordinates(peer.get)
-      val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
-      val m = visualizer.metrics()
-      val w = bounds.getWidth + m.pad_x
-      val h = bounds.getHeight + m.pad_y
+      val m = visualizer.metrics(g)
+      val bounds = m.string_bounds(visualizer.Caption(peer.get))
+      val w = bounds.getWidth + m.pad
+      val h = bounds.getHeight + m.pad
       new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
     }
 
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
     {
       val caption = visualizer.Caption(peer.get)
-      val bounds = g.getFontMetrics.getStringBounds(caption, g)
+      val m = visualizer.metrics(g)
+      val bounds = m.string_bounds(caption)
+
       val s = shape(g, visualizer, peer)
 
       val c = visualizer.node_color(peer)
@@ -49,7 +51,7 @@
       g.setColor(c.foreground)
       g.drawString(caption,
         (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
-        (s.getCenterY + 5).toFloat)
+        (s.getY + m.pad / 2 + m.ascent).toFloat)
     }
   }
 

--- a/src/Tools/Graphview/visualizer.scala	Thu Jan 01 21:23:01 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Fri Jan 02 19:54:13 2015 +0100
@@ -54,19 +54,19 @@
     gfx
   }
 
-  class Metrics private[Visualizer]
+  class Metrics private[Visualizer](f: Font, frc: FontRenderContext)
   {
-    private val f = font()
-    def string_bounds(s: String) = f.getStringBounds(s, font_render_context)
+    def string_bounds(s: String) = f.getStringBounds(s, frc)
     private val specimen = string_bounds("mix")
 
     def char_width: Double = specimen.getWidth / 3
-    def line_height: Double = specimen.getHeight
-    def gap_x: Double = char_width * 2.5
-    def pad_x: Double = char_width * 0.5
-    def pad_y: Double = line_height * 0.25
+    def height: Double = specimen.getHeight
+    def ascent: Double = font.getLineMetrics("", frc).getAscent
+    def gap: Double = specimen.getWidth
+    def pad: Double = char_width
   }
-  def metrics(): Metrics = new Metrics
+  def metrics(): Metrics = new Metrics(font(), font_render_context)
+  def metrics(gfx: Graphics2D): Metrics = new Metrics(gfx.getFont, gfx.getFontRenderContext)
 
 
   /* rendering parameters */
@@ -152,8 +152,8 @@
           val max_width =
             model.current_graph.iterator.map({ case (_, (info, _)) =>
               m.string_bounds(info.name).getWidth }).max
-          val box_distance = max_width + m.pad_x + m.gap_x
-          def box_height(n: Int): Double = (m.line_height + m.pad_y) * (5 max n)
+          val box_distance = max_width + m.pad + m.gap
+          def box_height(n: Int): Double = m.char_width * 1.5 * (5 max n)
 
           Layout.make(model.current_graph, box_distance, box_height _)
         }