1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 15:58:47 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 16:34:30 2014 +0100
     1.3 @@ -186,14 +186,39 @@
     1.4  
     1.5    /* font size */
     1.6  
     1.7 +  private object font_size
     1.8 +  {
     1.9 +    // owned by Swing thread
    1.10 +    private var last_view: Option[View] = None
    1.11 +    private var steps = 0
    1.12 +    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.13 +    {
    1.14 +      val view = last_view getOrElse jEdit.getActiveView()
    1.15 +      Rendering.font_size_change(view, i =>
    1.16 +        {
    1.17 +          var j = i
    1.18 +          while (steps != 0 && j > 0) {
    1.19 +            if (steps > 0)
    1.20 +              { j += (j / 10) max 1; steps -= 1 }
    1.21 +            else
    1.22 +              { j -= (j / 10) max 1; steps += 1 }
    1.23 +          }
    1.24 +          steps = 0
    1.25 +          j
    1.26 +        })
    1.27 +    }
    1.28 +    def step(view: View, i: Int) { last_view = Some(view); steps += i; delay.invoke() }
    1.29 +    def reset() { delay.revoke(); last_view = None; steps = 0 }
    1.30 +  }
    1.31 +
    1.32    def reset_font_size(view: View): Unit =
    1.33 +  {
    1.34 +    font_size.reset()
    1.35      Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
    1.36 +  }
    1.37  
    1.38 -  def increase_font_size(view: View): Unit =
    1.39 -    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
    1.40 -
    1.41 -  def decrease_font_size(view: View): Unit =
    1.42 -    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
    1.43 +  def increase_font_size(view: View): Unit = font_size.step(view, 1)
    1.44 +  def decrease_font_size(view: View): Unit = font_size.step(view, -1)
    1.45  
    1.46  
    1.47    /* structured edits */

     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 15:58:47 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 16:34:30 2014 +0100
     2.3 @@ -54,11 +54,14 @@
     2.4  
     2.5    def font_size_change(view: View, change: Int => Int)
     2.6    {
     2.7 -    val size = change(view_font_size()) max font_size0 min font_size1
     2.8 -    jEdit.setIntegerProperty("view.fontsize", size)
     2.9 -    jEdit.propertiesChanged()
    2.10 -    jEdit.saveSettings()
    2.11 -    view.getStatus.setMessageAndClear("Text font size: " + size)
    2.12 +    val size0 = view_font_size()
    2.13 +    val size = change(size0) max font_size0 min font_size1
    2.14 +    if (size != size0) {
    2.15 +      jEdit.setIntegerProperty("view.fontsize", size)
    2.16 +      jEdit.propertiesChanged()
    2.17 +      jEdit.saveSettings()
    2.18 +      view.getStatus.setMessageAndClear("Text font size: " + size)
    2.19 +    }
    2.20    }
    2.21  
    2.22