src/Tools/jEdit/src/isabelle.scala
changeset 55825 694833e3e4a0
parent 55824 22bc50a19afa
child 55827 8a881f83e206
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 18:33:49 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:39:27 2014 +0100
     1.3 @@ -192,17 +192,17 @@
     1.4      private var steps = 0
     1.5      private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
     1.6      {
     1.7 -      Rendering.font_size_change(i =>
     1.8 +      Font_Info.main_change(size =>
     1.9          {
    1.10 -          var j = i
    1.11 -          while (steps != 0 && j > 0) {
    1.12 +          var i = size.round
    1.13 +          while (steps != 0 && i > 0) {
    1.14              if (steps > 0)
    1.15 -              { j += (j / 10) max 1; steps -= 1 }
    1.16 +              { i += (i / 10) max 1; steps -= 1 }
    1.17              else
    1.18 -              { j -= (j / 10) max 1; steps += 1 }
    1.19 +              { i -= (i / 10) max 1; steps += 1 }
    1.20            }
    1.21            steps = 0
    1.22 -          j
    1.23 +          i.toFloat
    1.24          })
    1.25      }
    1.26      def step(i: Int) { steps += i; delay.invoke() }
    1.27 @@ -212,7 +212,7 @@
    1.28    def reset_font_size()
    1.29    {
    1.30      font_size.reset()
    1.31 -    Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
    1.32 +    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
    1.33    }
    1.34  
    1.35    def increase_font_size() { font_size.step(1) }