1.1 --- a/src/Tools/jEdit/src/actions.xml	Sat Mar 01 16:34:30 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/actions.xml	Sat Mar 01 18:33:49 2014 +0100
     1.3 @@ -34,27 +34,27 @@
     1.4  	</ACTION>
     1.5  	<ACTION NAME="isabelle.reset-font-size">
     1.6  	  <CODE>
     1.7 -	    isabelle.jedit.Isabelle.reset_font_size(view);
     1.8 +	    isabelle.jedit.Isabelle.reset_font_size();
     1.9  	  </CODE>
    1.10  	</ACTION>
    1.11  	<ACTION NAME="isabelle.increase-font-size">
    1.12  	  <CODE>
    1.13 -	    isabelle.jedit.Isabelle.increase_font_size(view);
    1.14 +	    isabelle.jedit.Isabelle.increase_font_size();
    1.15  	  </CODE>
    1.16  	</ACTION>
    1.17  	<ACTION NAME="isabelle.increase-font-size2">
    1.18  	  <CODE>
    1.19 -	    isabelle.jedit.Isabelle.increase_font_size(view);
    1.20 +	    isabelle.jedit.Isabelle.increase_font_size();
    1.21  	  </CODE>
    1.22  	</ACTION>
    1.23  	<ACTION NAME="isabelle.decrease-font-size">
    1.24  	  <CODE>
    1.25 -	    isabelle.jedit.Isabelle.decrease_font_size(view);
    1.26 +	    isabelle.jedit.Isabelle.decrease_font_size();
    1.27  	  </CODE>
    1.28  	</ACTION>
    1.29  	<ACTION NAME="isabelle.decrease-font-size2">
    1.30  	  <CODE>
    1.31 -	    isabelle.jedit.Isabelle.decrease_font_size(view);
    1.32 +	    isabelle.jedit.Isabelle.decrease_font_size();
    1.33  	  </CODE>
    1.34  	</ACTION>
    1.35  	<ACTION NAME="isabelle.complete">

     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 16:34:30 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 18:33:49 2014 +0100
     2.3 @@ -189,12 +189,10 @@
     2.4    private object font_size
     2.5    {
     2.6      // owned by Swing thread
     2.7 -    private var last_view: Option[View] = None
     2.8      private var steps = 0
     2.9      private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    2.10      {
    2.11 -      val view = last_view getOrElse jEdit.getActiveView()
    2.12 -      Rendering.font_size_change(view, i =>
    2.13 +      Rendering.font_size_change(i =>
    2.14          {
    2.15            var j = i
    2.16            while (steps != 0 && j > 0) {
    2.17 @@ -207,18 +205,18 @@
    2.18            j
    2.19          })
    2.20      }
    2.21 -    def step(view: View, i: Int) { last_view = Some(view); steps += i; delay.invoke() }
    2.22 -    def reset() { delay.revoke(); last_view = None; steps = 0 }
    2.23 +    def step(i: Int) { steps += i; delay.invoke() }
    2.24 +    def reset() { delay.revoke(); steps = 0 }
    2.25    }
    2.26  
    2.27 -  def reset_font_size(view: View): Unit =
    2.28 +  def reset_font_size()
    2.29    {
    2.30      font_size.reset()
    2.31 -    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
    2.32 +    Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
    2.33    }
    2.34  
    2.35 -  def increase_font_size(view: View): Unit = font_size.step(view, 1)
    2.36 -  def decrease_font_size(view: View): Unit = font_size.step(view, -1)
    2.37 +  def increase_font_size() { font_size.step(1) }
    2.38 +  def decrease_font_size() { font_size.step(-1) }
    2.39  
    2.40  
    2.41    /* structured edits */

     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 16:34:30 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 18:33:49 2014 +0100
     3.3 @@ -52,7 +52,7 @@
     3.4    def font_size(scale: String): Float =
     3.5      (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
     3.6  
     3.7 -  def font_size_change(view: View, change: Int => Int)
     3.8 +  def font_size_change(change: Int => Int)
     3.9    {
    3.10      val size0 = view_font_size()
    3.11      val size = change(size0) max font_size0 min font_size1
    3.12 @@ -60,7 +60,7 @@
    3.13        jEdit.setIntegerProperty("view.fontsize", size)
    3.14        jEdit.propertiesChanged()
    3.15        jEdit.saveSettings()
    3.16 -      view.getStatus.setMessageAndClear("Text font size: " + size)
    3.17 +      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    3.18      }
    3.19    }
    3.20