# HG changeset patch
# User wenzelm
# Date 1420497219 -3600
# Node ID bab9689559258f475b9a40e7498c7ddf664d5f0f
# Parent  d418ac9727f2c47db149bab9e5eb7fe16a1a2a5f# Parent  126293918a37ba04f4495ae3a7e6ed02b98f51e2
merged

diff -r d418ac9727f2 -r bab968955925 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -218,14 +218,14 @@
   def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
-  def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
+  def imitate_font(font: Font, family: String, scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
-    val size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight * font.getSize
-    font1.deriveFont((scale * size).toInt)
+    val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
+    new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
   }
 
-  def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String =
+  def imitate_font_css(font: Font, family: String, scale: Double = 1.0): String =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
diff -r d418ac9727f2 -r bab968955925 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/General/graph_display.ML	Mon Jan 05 23:33:39 2015 +0100
@@ -13,8 +13,6 @@
   val eq_entry: entry * entry -> bool
   val sort_graph: entry list -> entry list
   val write_graph_browser: Path.T -> entry list -> unit
-  val browserN: string
-  val graphviewN: string
   val display_graph: entry list -> unit
 end;
 
@@ -60,17 +58,6 @@
     in ((#2 key, node), map #2 (Graph.Keys.dest preds)) end));
 
 
-(* print modes *)
-
-val browserN = "browser";
-val graphviewN = "graphview";
-
-fun is_browser () =
-  (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
-    SOME m => m = browserN
-  | NONE => true);
-
-
 (* encode graph *)
 
 val encode_browser =
@@ -97,11 +84,18 @@
 val display_graph =
   sort_graph #> (fn entries =>
     let
-      val (markup, body) =
-        if is_browser () then (Markup.browserN, encode_browser entries)
-        else (Markup.graphviewN, YXML.string_of_body (encode_graph entries));
+      val ((bg1, bg2), en) =
+        YXML.output_markup_elem
+          (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+      val _ =
+        writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "new graph" ^ en);
+
       val ((bg1, bg2), en) =
-        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
-    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end);
+        YXML.output_markup_elem
+          (Active.make_markup Markup.browserN {implicit = false, properties = []});
+      val _ =
+        writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
+  in () end);
+
 
 end;
diff -r d418ac9727f2 -r bab968955925 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/build-jars	Mon Jan 05 23:33:39 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"
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/etc/options
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/etc/options	Mon Jan 05 23:33:39 2015 +0100
@@ -0,0 +1,12 @@
+(* :mode=isabelle-options: *)
+
+section "Graphview"
+
+option graphview_font_family : string = "Helvetica"
+  -- "base font family (notably for PDF)"
+
+option graphview_font_size : int = 12
+  -- "base font size (notably for PDF)"
+
+public option graphview_font_scale : real = 0.85
+  -- "scale factor of graph view wrt. main text font"
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 23:33:39 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 =>
+      Shapes.Node.shape(visualizer, node).contains(at))
 
   def refresh()
   {
@@ -100,7 +96,7 @@
       gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
       gfx.transform(Transform())
 
-      visualizer.Drawer.paint_all_visible(gfx, true)
+      visualizer.paint_all_visible(gfx)
     }
   }
   private val paint_panel = new Paint_Panel
@@ -132,7 +128,10 @@
     }
 
     def scale_discrete: Double =
-      (scale * visualizer.font_size).floor / visualizer.font_size
+    {
+      val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt
+      (scale * font_height).floor / font_height
+    }
 
     def apply() =
     {
@@ -144,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()
@@ -177,20 +176,12 @@
     }
 
     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.
+          collectFirst({
+            case (edge, (d, index))
+            if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index)
+          })
 
     def pressed(at: Point)
     {
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Jan 05 23:33:39 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,39 @@
 }
 
 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)
     }
+
+  def dummies_iterator: Iterator[Layout.Point] =
+    for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
 }
 
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -13,9 +13,7 @@
 import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser}
 
 import java.io.{File => JFile}
-import java.awt.{Color, Dimension, Graphics2D}
-import java.awt.geom.Rectangle2D
-import java.awt.image.BufferedImage
+import java.awt.{Color, Graphics2D}
 import javax.imageio.ImageIO
 import javax.swing.border.EmptyBorder
 import javax.swing.JComponent
@@ -45,6 +43,10 @@
         selected = visualizer.arrow_heads
         action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
       },
+      new CheckBox() {
+        selected = visualizer.show_dummies
+        action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+      },
       new Button {
         action = Action("Save image") {
           chooser.showSaveDialog(this) match {
@@ -72,9 +74,8 @@
     {
       gfx.setColor(Color.WHITE)
       gfx.fillRect(0, 0, w, h)
-
       gfx.translate(- box.x, - box.y)
-      visualizer.Drawer.paint_all_visible(gfx, false)
+      visualizer.paint_all_visible(gfx)
     }
 
     try {
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/metrics.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/metrics.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -0,0 +1,46 @@
+/*  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_x: Double = char_width * 1.5
+  def pad_y: Double = char_width
+
+  def box_width2(node: Graph_Display.Node): Double =
+    ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
+  def box_gap: Double = gap.ceil
+  def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
+}
+
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Mon Jan 05 23:33:39 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) =
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 23:33:39 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_x
+      val h = bounds.getHeight + metrics.pad_y
       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,40 +46,33 @@
       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)
     }
   }
 
   object Dummy
   {
-    private val identity = new AffineTransform()
-
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape =
+    def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
     {
-      val w = (m.space_width / 2).ceil
-      new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
+      val metrics = visualizer.metrics
+      val w = metrics.pad_x
+      new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
     }
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer): Unit =
-      paint_transformed(gfx, visualizer, identity)
-
-    def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
     {
-      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(shape(visualizer, d))
     }
   }
 
   object Straight_Edge
   {
-    def paint(gfx: Graphics2D, visualizer: Visualizer,
-      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
       val p = visualizer.Coordinates.get_node(edge._1)
       val q = visualizer.Coordinates.get_node(edge._2)
@@ -95,17 +88,15 @@
       ds.foreach(d => path.lineTo(d.x, d.y))
       path.lineTo(q.x, q.y)
 
-      if (dummies)
-        ds.foreach(d =>
-          Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+      if (visualizer.show_dummies)
+        ds.foreach(Dummy.paint(gfx, visualizer, _))
 
       gfx.setStroke(default_stroke)
       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 (visualizer.arrow_heads)
+        Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
     }
   }
 
@@ -113,8 +104,7 @@
   {
     private val slack = 0.1
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer,
-      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
       val p = visualizer.Coordinates.get_node(edge._1)
       val q = visualizer.Coordinates.get_node(edge._2)
@@ -125,7 +115,7 @@
         visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
       }
 
-      if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
+      if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
       else {
         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
         path.moveTo(p.x, p.y)
@@ -152,17 +142,15 @@
           q.x - slack * dx2, q.y - slack * dy2,
           q.x, q.y)
 
-        if (dummies)
-          ds.foreach(d =>
-            Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+        if (visualizer.show_dummies)
+          ds.foreach(Dummy.paint(gfx, visualizer, _))
 
         gfx.setStroke(default_stroke)
         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 (visualizer.arrow_heads)
+          Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
       }
     }
   }
diff -r d418ac9727f2 -r bab968955925 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 23:33:39 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(val model: Model)
+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,19 @@
 
   /* font rendering information */
 
-  def font_size: Int = 12
-  def font(): Font = new Font("Helvetica", Font.PLAIN, font_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)
+  def make_font(): Font =
+  {
+    val family = options.string("graphview_font_family")
+    val size = options.int("graphview_font_size")
+    new Font(family, Font.PLAIN, size)
+  }
 
 
   /* rendering parameters */
 
+  // owned by GUI thread
   var arrow_heads = false
+  var show_dummies = false
 
   object Colors
   {
@@ -105,12 +76,17 @@
     }
   }
 
+  def paint_all_visible(gfx: Graphics2D)
+  {
+    gfx.setRenderingHints(Metrics.rendering_hints)
+    for (edge <- visible_graph.edges_iterator)
+      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+    for (node <- visible_graph.keys_iterator)
+      Shapes.Node.paint(gfx, visualizer, node)
+  }
 
   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)
 
@@ -133,54 +109,36 @@
 
     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)
-        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
+      ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
+       (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
+         foreach(rect => {
+            x0 = x0 min rect.getMinX
+            y0 = y0 min rect.getMinY
+            x1 = x1 max rect.getMaxX
+            y1 = y1 max rect.getMaxY
+          })
+      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)
     }
   }
 
-  object Drawer
-  {
-    def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
-      if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
-
-    def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
-      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
-
-    def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
-    {
-      gfx.setFont(font())
-      gfx.setRenderingHints(rendering_hints)
-      val visible_graph = model.make_visible_graph()
-      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)
-  }
-
   object Selection
   {
     // owned by GUI thread
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Jan 05 23:33:39 2015 +0100
@@ -10,13 +10,13 @@
   -- "load all required files automatically to resolve theory imports"
 
 public option jedit_reset_font_size : int = 18
-  -- "reset font size for main text area"
+  -- "reset main text font size"
 
 public option jedit_font_scale : real = 1.0
-  -- "scale factor of add-on panels wrt. main text area"
+  -- "scale factor of add-on panels wrt. main text font"
 
 public option jedit_popup_font_scale : real = 0.85
-  -- "scale factor of popups wrt. main text area"
+  -- "scale factor of popups wrt. main text font"
 
 public option jedit_popup_bounds : real = 0.5
   -- "relative bounds of popup window wrt. logical screen size"
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -10,7 +10,7 @@
 import isabelle._
 
 import javax.swing.JComponent
-import java.awt.Point
+import java.awt.{Point, Font}
 import java.awt.event.{WindowFocusListener, WindowEvent}
 
 import org.gjt.sp.jedit.View
@@ -62,7 +62,7 @@
     graph_result match {
       case Exn.Res(graph) =>
         val model = new isabelle.graphview.Model(graph)
-        val visualizer = new isabelle.graphview.Visualizer(model) {
+        val visualizer = new isabelle.graphview.Visualizer(PIDE.options.value, model) {
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             Pretty_Tooltip.invoke(() =>
@@ -77,21 +77,41 @@
           override def background_color = view.getTextArea.getPainter.getBackground
           override def selection_color = view.getTextArea.getPainter.getSelectionColor
           override def error_color = PIDE.options.color_value("error_color")
-          override def font_size = view.getTextArea.getPainter.getFont.getSize
-          override def font = view.getTextArea.getPainter.getFont
+
+          override def make_font(): Font =
+            GUI.imitate_font(Font_Info.main().font,
+              PIDE.options.string("graphview_font_family"),
+              PIDE.options.real("graphview_font_scale"))
         }
         new isabelle.graphview.Main_Panel(model, visualizer)
       case Exn.Exn(exn) => new TextArea(Exn.message(exn))
     }
   set_content(graphview)
 
+
+  /* main */
+
+  private val main =
+    Session.Consumer[Session.Global_Options](getClass.getName) {
+      case _: Session.Global_Options =>
+        GUI_Thread.later {
+          graphview match {
+            case main_panel: isabelle.graphview.Main_Panel =>
+              main_panel.graph_panel.apply_layout()
+            case _ =>
+          }
+        }
+    }
+
   override def init()
   {
     GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    PIDE.session.global_options += main
   }
 
   override def exit()
   {
     GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    PIDE.session.global_options -= main
   }
 }
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -32,7 +32,7 @@
 
   class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
   {
-    private val css = GUI.imitate_font_css(Font_Info.main_family(), (new JLabel).getFont)
+    private val css = GUI.imitate_font_css((new JLabel).getFont, Font_Info.main_family())
 
     protected var _name = text
     protected var _start = int_to_pos(range.start)
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -201,7 +201,7 @@
         })
         setColumns(20)
         setToolTipText(search_label.tooltip)
-        setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+        setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
       })
 
   private val search_field_foreground = search_field.foreground
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -48,7 +48,7 @@
       { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
       setColumns(40)
       setToolTipText(tooltip)
-      setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
     }
 
 
diff -r d418ac9727f2 -r bab968955925 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jan 05 23:33:39 2015 +0100
@@ -124,7 +124,7 @@
         for (idx <- 0 until max_user_fonts)
           new_styles(user_font(idx, i.toByte)) = style
         for ((family, idx) <- Symbol.font_index)
-          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(family, _))
+          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
       }
       new_styles(hidden) =
         new SyntaxStyle(hidden_color, null,