tuned signature -- separate module Font_Info;
authorwenzelm
Sat Mar 01 19:39:27 2014 +0100 (2014-03-01)
changeset 55825694833e3e4a0
parent 55824 22bc50a19afa
child 55826 e56a52dd770a
tuned signature -- separate module Font_Info;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/symbols_dockable.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 01 18:33:49 2014 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Mar 01 19:39:27 2014 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4    "src/documentation_dockable.scala"
     1.5    "src/find_dockable.scala"
     1.6    "src/fold_handling.scala"
     1.7 +  "src/font_info.scala"
     1.8    "src/graphview_dockable.scala"
     1.9    "src/info_dockable.scala"
    1.10    "src/isabelle.scala"
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 18:33:49 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 19:39:27 2014 +0100
     2.3 @@ -196,7 +196,8 @@
     2.4        def open_popup(result: Completion.Result)
     2.5        {
     2.6          val font =
     2.7 -          painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
     2.8 +          painter.getFont.deriveFont(
     2.9 +            Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
    2.10  
    2.11          val range = result.range
    2.12          def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
     3.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
     3.3 @@ -56,8 +56,8 @@
     3.4    {
     3.5      Swing_Thread.require()
     3.6  
     3.7 -    pretty_text_area.resize(Rendering.font_family(),
     3.8 -      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
     3.9 +    pretty_text_area.resize(
    3.10 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    3.11    }
    3.12  
    3.13    private val delay_resize =
    3.14 @@ -121,7 +121,7 @@
    3.15      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
    3.16      setColumns(40)
    3.17      setToolTipText(query_label.tooltip)
    3.18 -    setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
    3.19 +    setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
    3.20    }
    3.21  
    3.22    private case class Context_Entry(val name: String, val description: String)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:39:27 2014 +0100
     4.3 @@ -0,0 +1,58 @@
     4.4 +/*  Title:      Tools/jEdit/src/jedit_font.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Font information, derived from main view font.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.jedit
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +
    4.16 +import java.awt.Font
    4.17 +
    4.18 +import org.gjt.sp.jedit.{jEdit, View}
    4.19 +
    4.20 +
    4.21 +object Font_Info
    4.22 +{
    4.23 +  val dummy: Font_Info = Font_Info("Dialog", 12.0f)
    4.24 +
    4.25 +
    4.26 +  /* size range */
    4.27 +
    4.28 +  val min_size = 5
    4.29 +  val max_size = 250
    4.30 +
    4.31 +  def restrict_size(size: Float): Float = size max min_size min max_size
    4.32 +
    4.33 +
    4.34 +  /* jEdit font */
    4.35 +
    4.36 +  def main_family(): String = jEdit.getProperty("view.font")
    4.37 +
    4.38 +  def main_size(scale: Double = 1.0): Float =
    4.39 +    restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
    4.40 +
    4.41 +  def main(scale: Double = 1.0): Font_Info =
    4.42 +    Font_Info(main_family(), main_size(scale))
    4.43 +
    4.44 +  def main_change(change: Float => Float)
    4.45 +  {
    4.46 +    val size0 = main_size()
    4.47 +    val size = restrict_size(change(size0)).round
    4.48 +    if (size != size0) {
    4.49 +      jEdit.setIntegerProperty("view.fontsize", size)
    4.50 +      jEdit.propertiesChanged()
    4.51 +      jEdit.saveSettings()
    4.52 +      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    4.53 +    }
    4.54 +  }
    4.55 +}
    4.56 +
    4.57 +sealed case class Font_Info(family: String, size: Float)
    4.58 +{
    4.59 +  def font: Font = new Font(family, Font.PLAIN, size.round)
    4.60 +}
    4.61 +
     5.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
     5.3 @@ -76,8 +76,8 @@
     5.4    {
     5.5      Swing_Thread.require()
     5.6  
     5.7 -    pretty_text_area.resize(Rendering.font_family(),
     5.8 -      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
     5.9 +    pretty_text_area.resize(
    5.10 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    5.11    }
    5.12  
    5.13  
     6.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 18:33:49 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:39:27 2014 +0100
     6.3 @@ -192,17 +192,17 @@
     6.4      private var steps = 0
     6.5      private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
     6.6      {
     6.7 -      Rendering.font_size_change(i =>
     6.8 +      Font_Info.main_change(size =>
     6.9          {
    6.10 -          var j = i
    6.11 -          while (steps != 0 && j > 0) {
    6.12 +          var i = size.round
    6.13 +          while (steps != 0 && i > 0) {
    6.14              if (steps > 0)
    6.15 -              { j += (j / 10) max 1; steps -= 1 }
    6.16 +              { i += (i / 10) max 1; steps -= 1 }
    6.17              else
    6.18 -              { j -= (j / 10) max 1; steps += 1 }
    6.19 +              { i -= (i / 10) max 1; steps += 1 }
    6.20            }
    6.21            steps = 0
    6.22 -          j
    6.23 +          i.toFloat
    6.24          })
    6.25      }
    6.26      def step(i: Int) { steps += i; delay.invoke() }
    6.27 @@ -212,7 +212,7 @@
    6.28    def reset_font_size()
    6.29    {
    6.30      font_size.reset()
    6.31 -    Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
    6.32 +    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
    6.33    }
    6.34  
    6.35    def increase_font_size() { font_size.step(1) }
     7.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 01 18:33:49 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 01 19:39:27 2014 +0100
     7.3 @@ -30,7 +30,7 @@
     7.4      protected var _end = int_to_pos(end)
     7.5      override def getIcon: Icon = null
     7.6      override def getShortString: String =
     7.7 -      "<html><span style=\"font-family: " + Rendering.font_family() + ";\">" +
     7.8 +      "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
     7.9        HTML.encode(_name) + "</span></html>"
    7.10      override def getLongString: String = _name
    7.11      override def getName: String = _name
     8.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
     8.3 @@ -41,8 +41,8 @@
     8.4    {
     8.5      Swing_Thread.require()
     8.6  
     8.7 -    pretty_text_area.resize(Rendering.font_family(),
     8.8 -      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
     8.9 +    pretty_text_area.resize(
    8.10 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    8.11    }
    8.12  
    8.13    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
     9.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 18:33:49 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 19:39:27 2014 +0100
     9.3 @@ -61,8 +61,7 @@
     9.4  
     9.5    Swing_Thread.require()
     9.6  
     9.7 -  private var current_font_family = "Dialog"
     9.8 -  private var current_font_size: Int = 12
     9.9 +  private var current_font_info: Font_Info = Font_Info.dummy
    9.10    private var current_body: XML.Body = Nil
    9.11    private var current_base_snapshot = Document.Snapshot.init
    9.12    private var current_base_results = Command.Results.empty
    9.13 @@ -80,18 +79,19 @@
    9.14    {
    9.15      Swing_Thread.require()
    9.16  
    9.17 -    val font = new Font(current_font_family, Font.PLAIN, current_font_size)
    9.18 +    val font = current_font_info.font
    9.19      getPainter.setFont(font)
    9.20      getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    9.21      getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
    9.22 -    getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
    9.23 +    getPainter.setStyles(
    9.24 +      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
    9.25  
    9.26      val fold_line_style = new Array[SyntaxStyle](4)
    9.27      for (i <- 0 to 3) {
    9.28        fold_line_style(i) =
    9.29          SyntaxUtilities.parseStyle(
    9.30            jEdit.getProperty("view.style.foldLine." + i),
    9.31 -          current_font_family, current_font_size, true)
    9.32 +          current_font_info.family, current_font_info.size.round, true)
    9.33      }
    9.34      getPainter.setFoldLineStyle(fold_line_style)
    9.35  
    9.36 @@ -139,12 +139,11 @@
    9.37      }
    9.38    }
    9.39  
    9.40 -  def resize(font_family: String, font_size: Int)
    9.41 +  def resize(font_info: Font_Info)
    9.42    {
    9.43      Swing_Thread.require()
    9.44  
    9.45 -    current_font_family = font_family
    9.46 -    current_font_size = font_size
    9.47 +    current_font_info = font_info
    9.48      refresh()
    9.49    }
    9.50  
    10.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 18:33:49 2014 +0100
    10.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 01 19:39:27 2014 +0100
    10.3 @@ -199,8 +199,7 @@
    10.4      }
    10.5    })
    10.6  
    10.7 -  pretty_text_area.resize(Rendering.font_family(),
    10.8 -    Rendering.font_size("jedit_popup_font_scale").round)
    10.9 +  pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
   10.10  
   10.11  
   10.12    /* main content */
    11.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 18:33:49 2014 +0100
    11.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 19:39:27 2014 +0100
    11.3 @@ -41,30 +41,6 @@
    11.4      Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    11.5  
    11.6  
    11.7 -  /* jEdit font */
    11.8 -
    11.9 -  def font_family(): String = jEdit.getProperty("view.font")
   11.10 -
   11.11 -  private def view_font_size(): Int = jEdit.getIntegerProperty("view.fontsize", 16)
   11.12 -  private val font_size0 = 5
   11.13 -  private val font_size1 = 250
   11.14 -
   11.15 -  def font_size(scale: String): Float =
   11.16 -    (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
   11.17 -
   11.18 -  def font_size_change(change: Int => Int)
   11.19 -  {
   11.20 -    val size0 = view_font_size()
   11.21 -    val size = change(size0) max font_size0 min font_size1
   11.22 -    if (size != size0) {
   11.23 -      jEdit.setIntegerProperty("view.fontsize", size)
   11.24 -      jEdit.propertiesChanged()
   11.25 -      jEdit.saveSettings()
   11.26 -      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
   11.27 -    }
   11.28 -  }
   11.29 -
   11.30 -
   11.31    /* popup window bounds */
   11.32  
   11.33    def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
    12.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
    12.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
    12.3 @@ -84,7 +84,7 @@
    12.4    private def do_paint()
    12.5    {
    12.6      Swing_Thread.later {
    12.7 -        text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
    12.8 +      text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    12.9      }
   12.10    }
   12.11  
    13.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Mar 01 18:33:49 2014 +0100
    13.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Mar 01 19:39:27 2014 +0100
    13.3 @@ -181,7 +181,7 @@
    13.4    def do_paint()
    13.5    {
    13.6      Swing_Thread.later {
    13.7 -      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
    13.8 +      area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    13.9      }
   13.10    }
   13.11  
    14.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
    14.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
    14.3 @@ -57,8 +57,8 @@
    14.4    {
    14.5      Swing_Thread.require()
    14.6  
    14.7 -    pretty_text_area.resize(Rendering.font_family(),
    14.8 -      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    14.9 +    pretty_text_area.resize(
   14.10 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   14.11    }
   14.12  
   14.13    private val delay_resize =
    15.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Mar 01 18:33:49 2014 +0100
    15.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Mar 01 19:39:27 2014 +0100
    15.3 @@ -26,7 +26,7 @@
    15.4    private class Symbol_Component(val symbol: String) extends Button
    15.5    {
    15.6      private val decoded = Symbol.decode(symbol)
    15.7 -    private val font_size = Rendering.font_size("jedit_font_scale").round
    15.8 +    private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
    15.9  
   15.10      font =
   15.11        Symbol.fonts.get(symbol) match {