# HG changeset patch
# User wenzelm
# Date 1393699167 -3600
# Node ID 694833e3e4a0e7cf9285e6ad41c7611d5c2a9b20
# Parent  22bc50a19afa9e3abeeb440430ecfaf57ec08c79
tuned signature -- separate module Font_Info;

diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 01 19:39:27 2014 +0100
@@ -16,6 +16,7 @@
   "src/documentation_dockable.scala"
   "src/find_dockable.scala"
   "src/fold_handling.scala"
+  "src/font_info.scala"
   "src/graphview_dockable.scala"
   "src/info_dockable.scala"
   "src/isabelle.scala"
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -196,7 +196,8 @@
       def open_popup(result: Completion.Result)
       {
         val font =
-          painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+          painter.getFont.deriveFont(
+            Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
 
         val range = result.range
         def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -56,8 +56,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(Rendering.font_family(),
-      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(
+      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   }
 
   private val delay_resize =
@@ -121,7 +121,7 @@
     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
     setColumns(40)
     setToolTipText(query_label.tooltip)
-    setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
+    setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
   }
 
   private case class Context_Entry(val name: String, val description: String)
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/font_info.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -0,0 +1,58 @@
+/*  Title:      Tools/jEdit/src/jedit_font.scala
+    Author:     Makarius
+
+Font information, derived from main view font.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import java.awt.Font
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+object Font_Info
+{
+  val dummy: Font_Info = Font_Info("Dialog", 12.0f)
+
+
+  /* size range */
+
+  val min_size = 5
+  val max_size = 250
+
+  def restrict_size(size: Float): Float = size max min_size min max_size
+
+
+  /* jEdit font */
+
+  def main_family(): String = jEdit.getProperty("view.font")
+
+  def main_size(scale: Double = 1.0): Float =
+    restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
+
+  def main(scale: Double = 1.0): Font_Info =
+    Font_Info(main_family(), main_size(scale))
+
+  def main_change(change: Float => Float)
+  {
+    val size0 = main_size()
+    val size = restrict_size(change(size0)).round
+    if (size != size0) {
+      jEdit.setIntegerProperty("view.fontsize", size)
+      jEdit.propertiesChanged()
+      jEdit.saveSettings()
+      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+    }
+  }
+}
+
+sealed case class Font_Info(family: String, size: Float)
+{
+  def font: Font = new Font(family, Font.PLAIN, size.round)
+}
+
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -76,8 +76,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(Rendering.font_family(),
-      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(
+      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   }
 
 
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -192,17 +192,17 @@
     private var steps = 0
     private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
     {
-      Rendering.font_size_change(i =>
+      Font_Info.main_change(size =>
         {
-          var j = i
-          while (steps != 0 && j > 0) {
+          var i = size.round
+          while (steps != 0 && i > 0) {
             if (steps > 0)
-              { j += (j / 10) max 1; steps -= 1 }
+              { i += (i / 10) max 1; steps -= 1 }
             else
-              { j -= (j / 10) max 1; steps += 1 }
+              { i -= (i / 10) max 1; steps += 1 }
           }
           steps = 0
-          j
+          i.toFloat
         })
     }
     def step(i: Int) { steps += i; delay.invoke() }
@@ -212,7 +212,7 @@
   def reset_font_size()
   {
     font_size.reset()
-    Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
+    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
   }
 
   def increase_font_size() { font_size.step(1) }
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -30,7 +30,7 @@
     protected var _end = int_to_pos(end)
     override def getIcon: Icon = null
     override def getShortString: String =
-      "<html><span style=\"font-family: " + Rendering.font_family() + ";\">" +
+      "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
       HTML.encode(_name) + "</span></html>"
     override def getLongString: String = _name
     override def getName: String = _name
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -41,8 +41,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(Rendering.font_family(),
-      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(
+      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   }
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -61,8 +61,7 @@
 
   Swing_Thread.require()
 
-  private var current_font_family = "Dialog"
-  private var current_font_size: Int = 12
+  private var current_font_info: Font_Info = Font_Info.dummy
   private var current_body: XML.Body = Nil
   private var current_base_snapshot = Document.Snapshot.init
   private var current_base_results = Command.Results.empty
@@ -80,18 +79,19 @@
   {
     Swing_Thread.require()
 
-    val font = new Font(current_font_family, Font.PLAIN, current_font_size)
+    val font = current_font_info.font
     getPainter.setFont(font)
     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
     getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
-    getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
+    getPainter.setStyles(
+      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
 
     val fold_line_style = new Array[SyntaxStyle](4)
     for (i <- 0 to 3) {
       fold_line_style(i) =
         SyntaxUtilities.parseStyle(
           jEdit.getProperty("view.style.foldLine." + i),
-          current_font_family, current_font_size, true)
+          current_font_info.family, current_font_info.size.round, true)
     }
     getPainter.setFoldLineStyle(fold_line_style)
 
@@ -139,12 +139,11 @@
     }
   }
 
-  def resize(font_family: String, font_size: Int)
+  def resize(font_info: Font_Info)
   {
     Swing_Thread.require()
 
-    current_font_family = font_family
-    current_font_size = font_size
+    current_font_info = font_info
     refresh()
   }
 
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -199,8 +199,7 @@
     }
   })
 
-  pretty_text_area.resize(Rendering.font_family(),
-    Rendering.font_size("jedit_popup_font_scale").round)
+  pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
 
 
   /* main content */
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -41,30 +41,6 @@
     Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
 
 
-  /* jEdit font */
-
-  def font_family(): String = jEdit.getProperty("view.font")
-
-  private def view_font_size(): Int = jEdit.getIntegerProperty("view.fontsize", 16)
-  private val font_size0 = 5
-  private val font_size1 = 250
-
-  def font_size(scale: String): Float =
-    (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
-
-  def font_size_change(change: Int => Int)
-  {
-    val size0 = view_font_size()
-    val size = change(size0) max font_size0 min font_size1
-    if (size != size0) {
-      jEdit.setIntegerProperty("view.fontsize", size)
-      jEdit.propertiesChanged()
-      jEdit.saveSettings()
-      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
-    }
-  }
-
-
   /* popup window bounds */
 
   def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -84,7 +84,7 @@
   private def do_paint()
   {
     Swing_Thread.later {
-        text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+      text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
     }
   }
 
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -181,7 +181,7 @@
   def do_paint()
   {
     Swing_Thread.later {
-      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
+      area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
     }
   }
 
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -57,8 +57,8 @@
   {
     Swing_Thread.require()
 
-    pretty_text_area.resize(Rendering.font_family(),
-      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
+    pretty_text_area.resize(
+      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   }
 
   private val delay_resize =
diff -r 22bc50a19afa -r 694833e3e4a0 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
@@ -26,7 +26,7 @@
   private class Symbol_Component(val symbol: String) extends Button
   {
     private val decoded = Symbol.decode(symbol)
-    private val font_size = Rendering.font_size("jedit_font_scale").round
+    private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
 
     font =
       Symbol.fonts.get(symbol) match {