src/Tools/jEdit/src/font_info.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 57044 042d6e58cb40
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Tools/jEdit/src/font_info.scala
     2     Author:     Makarius
     3 
     4 Font information, derived from main jEdit view font.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import java.awt.Font
    14 
    15 import org.gjt.sp.jedit.{jEdit, View}
    16 
    17 
    18 object Font_Info
    19 {
    20   /* size range */
    21 
    22   val min_size = 5
    23   val max_size = 250
    24 
    25   def restrict_size(size: Float): Float = size max min_size min max_size
    26 
    27 
    28   /* main jEdit font */
    29 
    30   def main_family(): String = jEdit.getProperty("view.font")
    31 
    32   def main_size(scale: Double = 1.0): Float =
    33     restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat)
    34 
    35   def main(scale: Double = 1.0): Font_Info =
    36     Font_Info(main_family(), main_size(scale))
    37 
    38 
    39   /* incremental size change */
    40 
    41   object main_change
    42   {
    43     private def change_size(change: Float => Float)
    44     {
    45       GUI_Thread.require {}
    46 
    47       val size0 = main_size()
    48       val size = restrict_size(change(size0)).round
    49       if (size != size0) {
    50         jEdit.setIntegerProperty("view.fontsize", size)
    51         jEdit.propertiesChanged()
    52         jEdit.saveSettings()
    53         jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    54       }
    55     }
    56 
    57     // owned by GUI thread
    58     private var steps = 0
    59     private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    60     {
    61       change_size(size =>
    62         {
    63           var i = size.round
    64           while (steps != 0 && i > 0) {
    65             if (steps > 0)
    66               { i += (i / 10) max 1; steps -= 1 }
    67             else
    68               { i -= (i / 10) max 1; steps += 1 }
    69           }
    70           steps = 0
    71           i.toFloat
    72         })
    73     }
    74 
    75     def step(i: Int)
    76     {
    77       steps += i
    78       delay.invoke()
    79     }
    80 
    81     def reset(size: Float)
    82     {
    83       delay.revoke()
    84       steps = 0
    85       change_size(_ => size)
    86     }
    87   }
    88 
    89 
    90   /* zoom box */
    91 
    92   abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" }
    93 }
    94 
    95 sealed case class Font_Info(family: String, size: Float)
    96 {
    97   def font: Font = new Font(family, Font.PLAIN, size.round)
    98 }
    99