separate module Metrics;
maintain static metrics (with font) and visible_graph via layout;

--- a/src/Pure/build-jars	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Pure/build-jars	Mon Jan 05 21:47:12 2015 +0100
@@ -106,6 +106,7 @@
   "../Tools/Graphview/graph_panel.scala"
   "../Tools/Graphview/layout.scala"
   "../Tools/Graphview/main_panel.scala"
+  "../Tools/Graphview/metrics.scala"
   "../Tools/Graphview/model.scala"
   "../Tools/Graphview/mutator_dialog.scala"
   "../Tools/Graphview/mutator_event.scala"

--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -12,7 +12,6 @@
 
 import java.awt.{Dimension, Graphics2D, Point}
 import java.awt.geom.{AffineTransform, Point2D}
-import java.awt.image.BufferedImage
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
 
 import scala.swing.{Panel, ScrollPane}
@@ -46,11 +45,8 @@
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
   def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
-  {
-    val m = visualizer.metrics()
-    visualizer.model.make_visible_graph().keys_iterator
-      .find(node => visualizer.Drawer.shape(m, node).contains(at))
-  }
+    visualizer.visible_graph.keys_iterator.find(node =>
+      visualizer.Drawer.shape(node).contains(at))
 
   def refresh()
   {
@@ -133,7 +129,7 @@
 
     def scale_discrete: Double =
     {
-      val font_height = GUI.line_metrics(visualizer.font()).getHeight.toInt
+      val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt
       (scale * font_height).floor / font_height
     }
 
@@ -147,7 +143,7 @@
 
     def fit_to_window()
     {
-      if (visualizer.model.make_visible_graph().is_empty)
+      if (visualizer.visible_graph.is_empty)
         rescale(1.0)
       else {
         val box = visualizer.Coordinates.bounding_box()
@@ -181,18 +177,16 @@
 
     def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
     {
-      val m = visualizer.metrics()
-      visualizer.model.make_visible_graph().edges_iterator.map(
-        edge =>
-          visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
-            {
-              case (_, (p, _)) =>
-                visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
-                  contains(at.getX() - p.x, at.getY() - p.y)
-            }) match {
-              case None => None
-              case Some((edge, (_, index))) => Some((edge, index))
-            }
+      visualizer.visible_graph.edges_iterator.map(edge =>
+        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
+          {
+            case (_, (p, _)) =>
+              visualizer.Drawer.shape(Graph_Display.Node.dummy).
+                contains(at.getX() - p.x, at.getY() - p.y)
+          }) match {
+            case None => None
+            case Some((edge, (_, index))) => Some((edge, index))
+          }
     }
 
     def pressed(at: Point)

--- a/src/Tools/Graphview/layout.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -27,12 +27,13 @@
   private type Level = List[Key]
   private type Levels = List[Level]
 
-  val empty = new Layout(Map.empty, Map.empty)
+  val empty: Layout =
+    new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty)
 
   val pendulum_iterations = 10
   val minimize_crossings_iterations = 40
 
-  def make(metrics: Visualizer.Metrics, visible_graph: Graph_Display.Graph): Layout =
+  def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout =
   {
     if (visible_graph.is_empty) empty
     else {
@@ -69,7 +70,7 @@
           case (map, key) => map + (key -> dummies(key).map(coords(_)))
         }
 
-      new Layout(coords, dummy_coords)
+      new Layout(metrics, visible_graph, coords, dummy_coords)
     }
   }
 
@@ -170,7 +171,7 @@
   }
 
   def pendulum(
-    metrics: Visualizer.Metrics, graph: Graph_Display.Graph,
+    metrics: Metrics, graph: Graph_Display.Graph,
     levels: Levels, coords: Map[Key, Point]): Coordinates =
   {
     type Regions = List[List[Region]]
@@ -252,7 +253,7 @@
   {
     var nodes: List[Key] = List(node)
 
-    def distance(metrics: Visualizer.Metrics, coords: Coordinates, that: Region): Double =
+    def distance(metrics: Metrics, coords: Coordinates, that: Region): Double =
     {
       val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1)
       val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2)
@@ -278,26 +279,36 @@
 }
 
 final class Layout private(
+  val metrics: Metrics,
+  val visible_graph: Graph_Display.Graph,
   nodes: Map[Graph_Display.Node, Layout.Point],
   dummies: Map[Graph_Display.Edge, List[Layout.Point]])
 {
+  /* nodes */
+
   def get_node(node: Graph_Display.Node): Layout.Point =
     nodes.getOrElse(node, Layout.Point.zero)
 
   def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
     nodes.get(node) match {
       case None => this
-      case Some(p) => new Layout(nodes + (node -> f(p)), dummies)
+      case Some(p) =>
+        val nodes1 = nodes + (node -> f(p))
+        new Layout(metrics, visible_graph, nodes1, dummies)
     }
 
 
+  /* dummies */
+
   def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
     dummies.getOrElse(edge, Nil)
 
   def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
     dummies.get(edge) match {
       case None => this
-      case Some(ds) => new Layout(nodes, dummies + (edge -> f(ds)))
+      case Some(ds) =>
+        val dummies1 = dummies + (edge -> f(ds))
+        new Layout(metrics, visible_graph, nodes, dummies1)
     }
 }
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/metrics.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -0,0 +1,45 @@
+/*  Title:      Tools/Graphview/metrics.scala
+    Author:     Makarius
+
+Physical metrics for layout and painting.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.{Font, RenderingHints}
+import java.awt.font.FontRenderContext
+
+
+object Metrics
+{
+  val rendering_hints: RenderingHints =
+    new RenderingHints(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
+
+  val font_render_context: FontRenderContext =
+    new FontRenderContext(null, true, false)
+
+  def apply(font: Font): Metrics = new Metrics(font)
+
+  val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12))
+}
+
+class Metrics private(val font: Font)
+{
+  def string_bounds(s: String) = font.getStringBounds(s, Metrics.font_render_context)
+  private val mix = string_bounds("mix")
+  val space_width = string_bounds(" ").getWidth
+  def char_width: Double = mix.getWidth / 3
+  def height: Double = mix.getHeight
+  def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
+  def gap: Double = mix.getWidth
+  def pad: Double = char_width
+
+  def box_width2(node: Graph_Display.Node): Double =
+    ((string_bounds(node.toString).getWidth + pad) / 2).ceil
+  def box_gap: Double = gap.ceil
+  def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
+}
+

--- a/src/Tools/Graphview/popups.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -24,7 +24,7 @@
     val visualizer = panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
-    val visible_graph = visualizer.model.make_visible_graph()
+    val visible_graph = visualizer.visible_graph
 
     def filter_context(
         nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =

--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -21,22 +21,22 @@
 
   object Node
   {
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
-      : Rectangle2D.Double =
+    def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
     {
+      val metrics = visualizer.metrics
       val p = visualizer.Coordinates.get_node(node)
-      val bounds = m.string_bounds(node.toString)
-      val w = bounds.getWidth + m.pad
-      val h = bounds.getHeight + m.pad
+      val bounds = metrics.string_bounds(node.toString)
+      val w = bounds.getWidth + metrics.pad
+      val h = bounds.getHeight + metrics.pad
       new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
     }
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
     {
-      val m = Visualizer.Metrics(gfx)
-      val s = shape(m, visualizer, node)
+      val metrics = visualizer.metrics
+      val s = shape(visualizer, node)
       val c = visualizer.node_color(node)
-      val bounds = m.string_bounds(node.toString)
+      val bounds = metrics.string_bounds(node.toString)
 
       gfx.setColor(c.background)
       gfx.fill(s)
@@ -46,9 +46,10 @@
       gfx.draw(s)
 
       gfx.setColor(c.foreground)
+      gfx.setFont(metrics.font)
       gfx.drawString(node.toString,
         (s.getCenterX - bounds.getWidth / 2).round.toInt,
-        (s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt)
+        (s.getCenterY - bounds.getHeight / 2 + metrics.ascent).round.toInt)
     }
   }
 
@@ -56,8 +57,9 @@
   {
     private val identity = new AffineTransform()
 
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape =
+    def shape(visualizer: Visualizer): Shape =
     {
+      val m = visualizer.metrics
       val w = (m.space_width / 2).ceil
       new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
     }
@@ -67,12 +69,9 @@
 
     def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
     {
-      val m = Visualizer.Metrics(gfx)
-      val s = shape(m, visualizer)
-
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.dummy_color)
-      gfx.draw(at.createTransformedShape(s))
+      gfx.draw(at.createTransformedShape(shape(visualizer)))
     }
   }
 
@@ -103,9 +102,7 @@
       gfx.setColor(visualizer.edge_color(edge))
       gfx.draw(path)
 
-      if (head)
-        Arrow_Head.paint(gfx, path,
-          visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2))
+      if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
     }
   }
 
@@ -160,9 +157,7 @@
         gfx.setColor(visualizer.edge_color(edge))
         gfx.draw(path)
 
-        if (head)
-          Arrow_Head.paint(gfx, path,
-            visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2))
+        if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
       }
     }
   }

--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -10,46 +10,21 @@
 
 import isabelle._
 
-import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D}
-import java.awt.font.FontRenderContext
-import java.awt.image.BufferedImage
+import java.awt.{Font, Color, Shape, Graphics2D}
 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 mix = string_bounds("mix")
-    val space_width = string_bounds(" ").getWidth
-    def char_width: Double = mix.getWidth / 3
-    def height: Double = mix.getHeight
-    def ascent: Double = font.getLineMetrics("", font_render_context).getAscent
-    def gap: Double = mix.getWidth
-    def pad: Double = char_width
-
-    def box_width2(node: Graph_Display.Node): Double =
-      ((string_bounds(node.toString).getWidth + pad) / 2).ceil
-    def box_gap: Double = gap.ceil
-    def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
-  }
-}
-
 class Visualizer(options: => Options, val model: Model)
 {
   visualizer =>
 
+  // owned by GUI thread
+  private var layout: Layout = Layout.empty
+
+  def metrics: Metrics = layout.metrics
+  def visible_graph: Graph_Display.Graph = layout.visible_graph
+
 
   /* tooltips */
 
@@ -67,23 +42,13 @@
 
   /* font rendering information */
 
-  def font(): Font =
+  def make_font(): Font =
   {
     val family = options.string("graphview_font_family")
     val size = options.int("graphview_font_size")
     new Font(family, Font.PLAIN, size)
   }
 
-  val rendering_hints =
-    new RenderingHints(
-      RenderingHints.KEY_ANTIALIASING,
-      RenderingHints.VALUE_ANTIALIAS_ON)
-
-  val font_render_context = new FontRenderContext(null, true, false)
-
-  def metrics(): Visualizer.Metrics =
-    Visualizer.Metrics(font(), font_render_context)
-
 
   /* rendering parameters */
 
@@ -112,9 +77,6 @@
 
   object Coordinates
   {
-    // owned by GUI thread
-    private var layout = Layout.empty
-
     def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node)
     def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge)
 
@@ -137,28 +99,31 @@
 
     def update_layout()
     {
+      val metrics = Metrics(make_font())
+      val visible_graph = model.make_visible_graph()
+
       // FIXME avoid expensive operation on GUI thread
-      layout = Layout.make(metrics(), model.make_visible_graph())
+      layout = Layout.make(metrics, visible_graph)
     }
 
     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 <- model.make_visible_graph().keys_iterator) {
-        val shape = Shapes.Node.shape(m, visualizer, node)
+      for (node <- visible_graph.keys_iterator) {
+        val shape = Shapes.Node.shape(visualizer, node)
         x0 = x0 min shape.getMinX
         y0 = y0 min shape.getMinY
         x1 = x1 max shape.getMaxX
         y1 = y1 max shape.getMaxY
       }
-      x0 = (x0 - m.gap).floor
-      y0 = (y0 - m.gap).floor
-      x1 = (x1 + m.gap).ceil
-      y1 = (y1 + m.gap).ceil
+      val gap = metrics.gap
+      x0 = (x0 - gap).floor
+      y0 = (y0 - gap).floor
+      x1 = (x1 + gap).ceil
+      y1 = (y1 + gap).ceil
       new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
     }
   }
@@ -173,16 +138,14 @@
 
     def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
     {
-      gfx.setFont(font())
-      gfx.setRenderingHints(rendering_hints)
-      val visible_graph = model.make_visible_graph()
+      gfx.setRenderingHints(Metrics.rendering_hints)
       visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
       visible_graph.keys_iterator.foreach(apply(gfx, _))
     }
 
-    def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
-      if (node.is_dummy) Shapes.Dummy.shape(m, visualizer)
-      else Shapes.Node.shape(m, visualizer, node)
+    def shape(node: Graph_Display.Node): Shape =
+      if (node.is_dummy) Shapes.Dummy.shape(visualizer)
+      else Shapes.Node.shape(visualizer, node)
   }
 
   object Selection

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -78,7 +78,7 @@
           override def selection_color = view.getTextArea.getPainter.getSelectionColor
           override def error_color = PIDE.options.color_value("error_color")
 
-          override def font() =
+          override def make_font(): Font =
             GUI.imitate_font(Font_Info.main().font,
               PIDE.options.string("graphview_font_family"),
               PIDE.options.real("graphview_font_scale"))