diff -r 0331b6d2ab0c -r 22bc50a19afa src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 16:34:30 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Sat Mar 01 18:33:49 2014 +0100 @@ -189,12 +189,10 @@ private object font_size { // owned by Swing thread - private var last_view: Option[View] = None private var steps = 0 private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { - val view = last_view getOrElse jEdit.getActiveView() - Rendering.font_size_change(view, i => + Rendering.font_size_change(i => { var j = i while (steps != 0 && j > 0) { @@ -207,18 +205,18 @@ j }) } - def step(view: View, i: Int) { last_view = Some(view); steps += i; delay.invoke() } - def reset() { delay.revoke(); last_view = None; steps = 0 } + def step(i: Int) { steps += i; delay.invoke() } + def reset() { delay.revoke(); steps = 0 } } - def reset_font_size(view: View): Unit = + def reset_font_size() { font_size.reset() - Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size")) + Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size")) } - def increase_font_size(view: View): Unit = font_size.step(view, 1) - def decrease_font_size(view: View): Unit = font_size.step(view, -1) + def increase_font_size() { font_size.step(1) } + def decrease_font_size() { font_size.step(-1) } /* structured edits */