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