# HG changeset patch
# User wenzelm
# Date 1355257717 -3600
# Node ID 1cb983bccb5bd0c829eb66eef0266c1be07264c9
# Parent  8cc351df4a232f187cf0162ca28a856c5d357c9b
more official graphics context with font metrics;

diff -r 8cc351df4a23 -r 1cb983bccb5b src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Tue Dec 11 21:05:38 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala	Tue Dec 11 21:28:37 2012 +0100
@@ -45,14 +45,9 @@
   horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
 
-  private val gfx_aux =
-    new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
-  gfx_aux.setFont(visualizer.font)
-  gfx_aux.setRenderingHints(visualizer.rendering_hints)
-
   def node(at: Point2D): Option[String] =
     visualizer.model.visible_nodes()
-      .find(name => visualizer.Drawer.shape(gfx_aux, Some(name)).contains(at))
+      .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
 
   def refresh()
   {
@@ -193,7 +188,7 @@
             i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
           }).flatten.find({
             case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(gfx_aux, None).contains(at.getX() - x, at.getY() - y)
+              visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y)
           }) match {
             case None => None
             case Some((name, (_, index))) => Some((name, index))
diff -r 8cc351df4a23 -r 1cb983bccb5b src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Tue Dec 11 21:05:38 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Tue Dec 11 21:28:37 2012 +0100
@@ -10,7 +10,8 @@
 import isabelle._
 
 
-import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D, Toolkit}
+import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
+import java.awt.image.BufferedImage
 import javax.swing.JComponent
 
 
@@ -18,19 +19,24 @@
 {
   visualizer =>
 
+
   /* font rendering information */
 
   val font_family: String = "IsabelleText"
   val font_size: Int = 14
-
-  val font = new Font(visualizer.font_family, Font.BOLD, visualizer.font_size)
-  val font_metrics: FontMetrics = Toolkit.getDefaultToolkit.getFontMetrics(font)
+  val font = new Font(font_family, Font.BOLD, font_size)
 
   val rendering_hints =
     new RenderingHints(
       RenderingHints.KEY_ANTIALIASING,
       RenderingHints.VALUE_ANTIALIAS_ON)
 
+  val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics
+  gfx.setFont(font)
+  gfx.setRenderingHints(rendering_hints)
+
+  val font_metrics: FontMetrics = gfx.getFontMetrics(font)
+
   val tooltip_font_size: Int = 10
 
 
@@ -119,7 +125,7 @@
           val max_width =
             model.current.entries.map({ case (_, (info, _)) =>
               font_metrics.stringWidth(info.name).toDouble }).max
-          val box_distance = max_width + visualizer.pad_x + visualizer.gap_x
+          val box_distance = max_width + pad_x + gap_x
           def box_height(n: Int): Double =
             ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble
           Layout_Pendulum(model.current, box_distance, box_height)