# HG changeset patch
# User wenzelm
# Date 1420463618 -3600
# Node ID ac74eedb910aa3729f257a8aa53bcf666f61e702
# Parent  d0d0953e063f48f283f4c42fe00317c69f35900b
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
some graphview font options: Helvetica family is important for self-contained PDF;
tuned;

diff -r d0d0953e063f -r ac74eedb910a src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/Graphview/etc/options
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/etc/options	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 14:13:38 2015 +0100
@@ -132,7 +132,10 @@
     }
 
     def scale_discrete: Double =
-      (scale * visualizer.font_size).floor / visualizer.font_size
+    {
+      val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble
+      (scale * font_height).floor / font_height
+    }
 
     def apply() =
     {
diff -r d0d0953e063f -r ac74eedb910a src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 14:13:38 2015 +0100
@@ -46,7 +46,7 @@
   }
 }
 
-class Visualizer(val model: Model)
+class Visualizer(options: => Options, val model: Model)
 {
   visualizer =>
 
@@ -67,8 +67,12 @@
 
   /* font rendering information */
 
-  def font_size: Int = 12
-  def font(): Font = new Font("Helvetica", Font.PLAIN, font_size)
+  def 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(
diff -r d0d0953e063f -r ac74eedb910a src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 14:13:38 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,8 +77,11 @@
           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 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))
diff -r d0d0953e063f -r ac74eedb910a src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Jan 05 14:13:38 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 d0d0953e063f -r ac74eedb910a src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jan 05 14:13:38 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,