clarified bounding box, similar to old graph browser;
default font like old browser;
clarified metrics;
tuned signature;

--- a/src/Tools/Graphview/graph_panel.scala	Fri Jan 02 21:19:34 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sat Jan 03 13:11:10 2015 +0100
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Dimension, Graphics2D, Point, Rectangle}
+import java.awt.{Dimension, Graphics2D, Point}
 import java.awt.geom.{AffineTransform, Point2D}
 import java.awt.image.BufferedImage
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
@@ -45,9 +45,9 @@
 
   def node(at: Point2D): Option[String] =
   {
-    val gfx = visualizer.graphics_context()
+    val m = visualizer.metrics()
     visualizer.model.visible_nodes_iterator
-      .find(name => visualizer.Drawer.shape(gfx, Some(name)).contains(at))
+      .find(name => visualizer.Drawer.shape(m, Some(name)).contains(at))
   }
 
   def refresh()
@@ -78,14 +78,11 @@
   {
     def set_preferred_size()
     {
-      val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
+      val box = visualizer.Coordinates.bounding_box()
       val s = Transform.scale_discrete
-      val (px, py) = Transform.padding
 
       preferredSize =
-        new Dimension(
-          (math.abs(maxX - minX + px) * s).toInt,
-          (math.abs(maxY - minY + py) * s).toInt)
+        new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
 
       revalidate()
     }
@@ -124,23 +121,20 @@
 
   private object Transform
   {
-    val padding = (100, 40)
-
     private var _scale: Double = 1.0
     def scale: Double = _scale
     def scale_=(s: Double)
     {
-      _scale = (s min 10) max 0.1
+      _scale = (s min 10.0) max 0.1
     }
     def scale_discrete: Double =
       (_scale * visualizer.font_size).round.toDouble / visualizer.font_size
 
     def apply() =
     {
-      val (minX, minY, _, _) = visualizer.Coordinates.bounds()
-
+      val box = visualizer.Coordinates.bounding_box()
       val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
-      at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
+      at.translate(- box.x, - box.y)
       at
     }
 
@@ -149,11 +143,8 @@
       if (visualizer.model.visible_nodes_iterator.isEmpty)
         rescale(1.0)
       else {
-        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
-
-        val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
-        val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
-        rescale(sx min sy)
+        val box = visualizer.Coordinates.bounding_box()
+        rescale((size.width / box.width) min (size.height / box.height))
       }
     }
 
@@ -204,11 +195,11 @@
 
       def dummy(at: Point2D): Option[Dummy] =
       {
-        val gfx = visualizer.graphics_context()
+        val m = visualizer.metrics()
         visualizer.model.visible_edges_iterator.map(
           i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({
             case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(gfx, None).contains(at.getX() - x, at.getY() - y)
+              visualizer.Drawer.shape(m, None).contains(at.getX() - x, at.getY() - y)
           }) match {
             case None => None
             case Some((name, (_, index))) => Some((name, index))

--- a/src/Tools/Graphview/main_panel.scala	Fri Jan 02 21:19:34 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Sat Jan 03 13:11:10 2015 +0100
@@ -83,16 +83,16 @@
 
   private def export(file: JFile)
   {
-    val (x0, y0, x1, y1) = visualizer.Coordinates.bounds
-    val w = (math.abs(x1 - x0) + 400).toInt
-    val h = (math.abs(y1 - y0) + 200).toInt
+    val box = visualizer.Coordinates.bounding_box()
+    val w = box.width.ceil.toInt
+    val h = box.height.ceil.toInt
 
     def paint(gfx: Graphics2D)
     {
       gfx.setColor(Color.WHITE)
-      gfx.fill(new Rectangle2D.Double(0, 0, w, h))
+      gfx.fillRect(0, 0, w, h)
 
-      gfx.translate(- x0 + 200, - y0 + 100)
+      gfx.translate(- box.x, - box.y)
       visualizer.Drawer.paint_all_visible(gfx, false)
     }
 

--- a/src/Tools/Graphview/shapes.scala	Fri Jan 02 21:19:34 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 13:11:10 2015 +0100
@@ -16,7 +16,7 @@
 {
   trait Node
   {
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
   }
 
@@ -25,10 +25,10 @@
     private val stroke =
       new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String])
+      : Rectangle2D.Double =
     {
       val (x, y) = visualizer.Coordinates(peer.get)
-      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
@@ -38,10 +38,10 @@
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
     {
       val caption = visualizer.Caption(peer.get)
-      val m = visualizer.metrics(g)
+      val m = Visualizer.Metrics(g)
       val bounds = m.string_bounds(caption)
 
-      val s = shape(g, visualizer, peer)
+      val s = shape(m, visualizer, peer)
 
       val c = visualizer.node_color(peer)
       g.setStroke(stroke)
@@ -60,10 +60,10 @@
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-    private val shape = new Rectangle2D.Double(-5, -5, 10, 10)
+    private val shape = new Rectangle2D.Double(-5, -5, 10, 10)  // FIXME
     private val identity = new AffineTransform()
 
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape = shape
 
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
       paint_transformed(g, visualizer, peer, identity)
@@ -118,7 +118,8 @@
       g.setColor(visualizer.edge_color(peer))
       g.draw(path)
 
-      if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
+      if (head)
+        Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
     }
   }
 
@@ -178,7 +179,8 @@
         g.setColor(visualizer.edge_color(peer))
         g.draw(path)
 
-        if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
+        if (head)
+          Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
       }
     }
   }

--- a/src/Tools/Graphview/visualizer.scala	Fri Jan 02 21:19:34 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 13:11:10 2015 +0100
@@ -13,9 +13,34 @@
 import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D}
 import java.awt.font.FontRenderContext
 import java.awt.image.BufferedImage
+import java.awt.geom.Rectangle2D
 import javax.swing.JComponent
 
 
+object Visualizer
+{
+  object Metrics
+  {
+    def apply(font: Font, font_render_context: FontRenderContext) =
+      new Metrics(font, font_render_context)
+
+    def apply(gfx: Graphics2D): Metrics =
+      new Metrics(gfx.getFont, gfx.getFontRenderContext)
+  }
+
+  class Metrics private(font: Font, font_render_context: FontRenderContext)
+  {
+    def string_bounds(s: String) = font.getStringBounds(s, font_render_context)
+    private val specimen = string_bounds("mix")
+
+    def char_width: Double = specimen.getWidth / 3
+    def height: Double = specimen.getHeight
+    def ascent: Double = font.getLineMetrics("", font_render_context).getAscent
+    def gap: Double = specimen.getWidth
+    def pad: Double = char_width
+  }
+}
+
 class Visualizer(val model: Model)
 {
   visualizer =>
@@ -37,8 +62,8 @@
 
   /* font rendering information */
 
-  def font_size: Int = 14
-  def font(): Font = new Font("IsabelleText", Font.BOLD, font_size)
+  def font_size: Int = 12
+  def font(): Font = new Font("Helvetica", Font.PLAIN, font_size)
 
   val rendering_hints =
     new RenderingHints(
@@ -47,27 +72,8 @@
 
   val font_render_context = new FontRenderContext(null, true, false)
 
-  def graphics_context(): Graphics2D =
-  {
-    val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics
-    gfx.setFont(font())
-    gfx.setRenderingHints(rendering_hints)
-    gfx
-  }
-
-  class Metrics private[Visualizer](f: Font, frc: FontRenderContext)
-  {
-    def string_bounds(s: String) = f.getStringBounds(s, frc)
-    private val specimen = string_bounds("mix")
-
-    def char_width: Double = specimen.getWidth / 3
-    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(font(), font_render_context)
-  def metrics(gfx: Graphics2D): Metrics = new Metrics(gfx.getFont, gfx.getFontRenderContext)
+  def metrics(): Visualizer.Metrics =
+    Visualizer.Metrics(font(), font_render_context)
 
 
   /* rendering parameters */
@@ -100,10 +106,7 @@
     private var layout = Layout.empty
 
     def apply(k: String): (Double, Double) =
-      layout.nodes.get(k) match {
-        case Some(c) => c
-        case None => (0, 0)
-      }
+      layout.nodes.getOrElse(k, (0.0, 0.0))
 
     def apply(e: (String, String)): List[(Double, Double)] =
       layout.dummies.get(e) match {
@@ -160,16 +163,26 @@
         }
     }
 
-    def bounds(): (Double, Double, Double, Double) =
-      model.visible_nodes_iterator.toList match {
-        case Nil => (0, 0, 0, 0)
-        case nodes =>
-          val X: (String => Double) = (n => apply(n)._1)
-          val Y: (String => Double) = (n => apply(n)._2)
-
-          (X(nodes.minBy(X)), Y(nodes.minBy(Y)),
-           X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
+    def bounding_box(): Rectangle2D.Double =
+    {
+      val m = metrics()
+      var x0 = 0.0
+      var y0 = 0.0
+      var x1 = 0.0
+      var y1 = 0.0
+      for (node_name <- model.visible_nodes_iterator) {
+        val shape = Shapes.Growing_Node.shape(m, visualizer, Some(node_name))
+        x0 = x0 min shape.getMinX
+        y0 = y0 min shape.getMinY
+        x1 = x1 max shape.getMaxX
+        y1 = y1 max shape.getMaxY
       }
+      x0 = x0 - m.gap
+      y0 = y0 - m.gap
+      x1 = x1 + m.gap
+      y1 = y1 + m.gap
+      new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
+    }
   }
 
   object Drawer
@@ -202,11 +215,9 @@
         })
     }
 
-    def shape(g: Graphics2D, n: Option[String]): Shape =
-      n match {
-        case None => Shapes.Dummy.shape(g, visualizer, None)
-        case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n)
-      }
+    def shape(m: Visualizer.Metrics, n: Option[String]): Shape =
+      if (n.isEmpty) Shapes.Dummy.shape(m, visualizer, n)
+      else Shapes.Growing_Node.shape(m, visualizer, n)
   }
 
   object Selection