src/Tools/jEdit/src/font_info.scala
changeset 55827 8a881f83e206
parent 55826 e56a52dd770a
child 56662 f373fb77e0a4
     1.1 --- a/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:43:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:55:01 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -/*  Title:      Tools/jEdit/src/jedit_font.scala
     1.5 +/*  Title:      Tools/jEdit/src/font_info.scala
     1.6      Author:     Makarius
     1.7  
     1.8 -Font information, derived from main view font.
     1.9 +Font information, derived from main jEdit view font.
    1.10  */
    1.11  
    1.12  package isabelle.jedit
    1.13 @@ -25,7 +25,7 @@
    1.14    def restrict_size(size: Float): Float = size max min_size min max_size
    1.15  
    1.16  
    1.17 -  /* jEdit font */
    1.18 +  /* main jEdit font */
    1.19  
    1.20    def main_family(): String = jEdit.getProperty("view.font")
    1.21  
    1.22 @@ -35,15 +35,54 @@
    1.23    def main(scale: Double = 1.0): Font_Info =
    1.24      Font_Info(main_family(), main_size(scale))
    1.25  
    1.26 -  def main_change(change: Float => Float)
    1.27 +
    1.28 +  /* incremental size change */
    1.29 +
    1.30 +  object main_change
    1.31    {
    1.32 -    val size0 = main_size()
    1.33 -    val size = restrict_size(change(size0)).round
    1.34 -    if (size != size0) {
    1.35 -      jEdit.setIntegerProperty("view.fontsize", size)
    1.36 -      jEdit.propertiesChanged()
    1.37 -      jEdit.saveSettings()
    1.38 -      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    1.39 +    private def change_size(change: Float => Float)
    1.40 +    {
    1.41 +      Swing_Thread.require()
    1.42 +
    1.43 +      val size0 = main_size()
    1.44 +      val size = restrict_size(change(size0)).round
    1.45 +      if (size != size0) {
    1.46 +        jEdit.setIntegerProperty("view.fontsize", size)
    1.47 +        jEdit.propertiesChanged()
    1.48 +        jEdit.saveSettings()
    1.49 +        jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    1.50 +      }
    1.51 +    }
    1.52 +
    1.53 +    // owned by Swing thread
    1.54 +    private var steps = 0
    1.55 +    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.56 +    {
    1.57 +      change_size(size =>
    1.58 +        {
    1.59 +          var i = size.round
    1.60 +          while (steps != 0 && i > 0) {
    1.61 +            if (steps > 0)
    1.62 +              { i += (i / 10) max 1; steps -= 1 }
    1.63 +            else
    1.64 +              { i -= (i / 10) max 1; steps += 1 }
    1.65 +          }
    1.66 +          steps = 0
    1.67 +          i.toFloat
    1.68 +        })
    1.69 +    }
    1.70 +
    1.71 +    def step(i: Int)
    1.72 +    {
    1.73 +      steps += i
    1.74 +      delay.invoke()
    1.75 +    }
    1.76 +
    1.77 +    def reset(size: Float)
    1.78 +    {
    1.79 +      delay.revoke()
    1.80 +      steps = 0
    1.81 +      change_size(_ => size)
    1.82      }
    1.83    }
    1.84  }