# HG changeset patch
# User wenzelm
# Date 1420141820 -3600
# Node ID 6dea47cf6c6b895be06d34ec434bf3f8afe4226e
# Parent  cae3ef2897f2ff00067b5a584ec5e52ddcbca9f5
more dynamic visualizer -- re-use jEdit font info;

diff -r cae3ef2897f2 -r 6dea47cf6c6b src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 17:27:52 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 20:50:20 2015 +0100
@@ -46,8 +46,11 @@
   verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
 
   def node(at: Point2D): Option[String] =
+  {
+    val gfx = visualizer.graphics_context()
     visualizer.model.visible_nodes_iterator
-      .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
+      .find(name => visualizer.Drawer.shape(gfx, Some(name)).contains(at))
+  }
 
   def refresh()
   {
@@ -205,14 +208,17 @@
       }
 
       def dummy(at: Point2D): Option[Dummy] =
+      {
+        val gfx = visualizer.graphics_context()
         visualizer.model.visible_edges_iterator.map(
           i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({
             case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y)
+              visualizer.Drawer.shape(gfx, None).contains(at.getX() - x, at.getY() - y)
           }) match {
             case None => None
             case Some((name, (_, index))) => Some((name, index))
           }
+      }
 
       def pressed(at: Point)
       {
diff -r cae3ef2897f2 -r 6dea47cf6c6b src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Thu Jan 01 17:27:52 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Thu Jan 01 20:50:20 2015 +0100
@@ -28,8 +28,9 @@
     {
       val (x, y) = visualizer.Coordinates(peer.get)
       val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
-      val w = bounds.getWidth + visualizer.pad_x
-      val h = bounds.getHeight + visualizer.pad_y
+      val m = visualizer.metrics()
+      val w = bounds.getWidth + m.pad_x
+      val h = bounds.getHeight + m.pad_y
       new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
     }
 
diff -r cae3ef2897f2 -r 6dea47cf6c6b src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Thu Jan 01 17:27:52 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Thu Jan 01 20:50:20 2015 +0100
@@ -10,6 +10,7 @@
 import isabelle._
 
 import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D}
+import java.awt.font.FontRenderContext
 import java.awt.image.BufferedImage
 import javax.swing.JComponent
 
@@ -30,30 +31,41 @@
 
   /* font rendering information */
 
-  val font_family: String = "IsabelleText"
-  val font_size: Int = 14
-  val font = new Font(font_family, Font.BOLD, font_size)
+  def font_size: Int = 14
+  def font(): Font = new Font("IsabelleText", 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_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
+  }
 
-  val font_metrics: FontMetrics = gfx.getFontMetrics(font)
+  class Metrics private[Visualizer]
+  {
+    private val f = font()
+    def string_bounds(s: String) = f.getStringBounds(s, font_render_context)
+    private val specimen = string_bounds("mix")
 
-  val tooltip_font_size: Int = 10
+    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 metrics(): Metrics = new Metrics
 
 
   /* rendering parameters */
 
-  val gap_x = 20
-  val pad_x = 8
-  val pad_y = 5
-
   var arrow_heads = false
 
   object Colors
@@ -130,13 +142,15 @@
       layout =
         if (model.current_graph.is_empty) Layout_Pendulum.empty_layout
         else {
+          val m = metrics()
+
           val max_width =
             model.current_graph.iterator.map({ case (_, (info, _)) =>
-              font_metrics.stringWidth(info.name).toDouble }).max
-          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_graph, box_distance, box_height)
+              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)
+
+          Layout_Pendulum(model.current_graph, box_distance, box_height _)
         }
     }
 
diff -r cae3ef2897f2 -r 6dea47cf6c6b src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 17:27:52 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 20:50:20 2015 +0100
@@ -67,6 +67,8 @@
           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
         }
         new isabelle.graphview.Main_Panel(model, visualizer) {
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =