src/Tools/jEdit/src/font_info.scala
author wenzelm
Sat Mar 01 19:55:01 2014 +0100 (2014-03-01)
changeset 55827 8a881f83e206
parent 55826 e56a52dd770a
child 56662 f373fb77e0a4
permissions -rw-r--r--
clarified module structure;
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@55827
    45
      Swing_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@55827
    57
    // owned by Swing thread
wenzelm@55827
    58
    private var steps = 0
wenzelm@55827
    59
    private val delay = Swing_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@55825
    88
}
wenzelm@55825
    89
wenzelm@55825
    90
sealed case class Font_Info(family: String, size: Float)
wenzelm@55825
    91
{
wenzelm@55825
    92
  def font: Font = new Font(family, Font.PLAIN, size.round)
wenzelm@55825
    93
}
wenzelm@55825
    94