src/Tools/jEdit/src/isabelle.scala
changeset 55827 8a881f83e206
parent 55825 694833e3e4a0
child 56170 638b29331549
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:43:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:55:01 2014 +0100
     1.3 @@ -186,37 +186,11 @@
     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 steps = 0
    1.11 -    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.12 -    {
    1.13 -      Font_Info.main_change(size =>
    1.14 -        {
    1.15 -          var i = size.round
    1.16 -          while (steps != 0 && i > 0) {
    1.17 -            if (steps > 0)
    1.18 -              { i += (i / 10) max 1; steps -= 1 }
    1.19 -            else
    1.20 -              { i -= (i / 10) max 1; steps += 1 }
    1.21 -          }
    1.22 -          steps = 0
    1.23 -          i.toFloat
    1.24 -        })
    1.25 -    }
    1.26 -    def step(i: Int) { steps += i; delay.invoke() }
    1.27 -    def reset() { delay.revoke(); steps = 0 }
    1.28 +  def reset_font_size() {
    1.29 +    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
    1.30    }
    1.31 -
    1.32 -  def reset_font_size()
    1.33 -  {
    1.34 -    font_size.reset()
    1.35 -    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
    1.36 -  }
    1.37 -
    1.38 -  def increase_font_size() { font_size.step(1) }
    1.39 -  def decrease_font_size() { font_size.step(-1) }
    1.40 +  def increase_font_size() { Font_Info.main_change.step(1) }
    1.41 +  def decrease_font_size() { Font_Info.main_change.step(-1) }
    1.42  
    1.43  
    1.44    /* structured edits */