# HG changeset patch
# User wenzelm
# Date 1393695229 -3600
# Node ID 22bc50a19afa9e3abeeb440430ecfaf57ec08c79
# Parent  0331b6d2ab0c6b9dcf73f741daba709c31fa1da1
tuned;

diff -r 0331b6d2ab0c -r 22bc50a19afa src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Sat Mar 01 16:34:30 2014 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Sat Mar 01 18:33:49 2014 +0100
@@ -34,27 +34,27 @@
 	</ACTION>
 	<ACTION NAME="isabelle.reset-font-size">
 	  <CODE>
-	    isabelle.jedit.Isabelle.reset_font_size(view);
+	    isabelle.jedit.Isabelle.reset_font_size();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.increase-font-size">
 	  <CODE>
-	    isabelle.jedit.Isabelle.increase_font_size(view);
+	    isabelle.jedit.Isabelle.increase_font_size();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.increase-font-size2">
 	  <CODE>
-	    isabelle.jedit.Isabelle.increase_font_size(view);
+	    isabelle.jedit.Isabelle.increase_font_size();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.decrease-font-size">
 	  <CODE>
-	    isabelle.jedit.Isabelle.decrease_font_size(view);
+	    isabelle.jedit.Isabelle.decrease_font_size();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.decrease-font-size2">
 	  <CODE>
-	    isabelle.jedit.Isabelle.decrease_font_size(view);
+	    isabelle.jedit.Isabelle.decrease_font_size();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.complete">
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 */
diff -r 0331b6d2ab0c -r 22bc50a19afa src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 16:34:30 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 18:33:49 2014 +0100
@@ -52,7 +52,7 @@
   def font_size(scale: String): Float =
     (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
 
-  def font_size_change(view: View, change: Int => Int)
+  def font_size_change(change: Int => Int)
   {
     val size0 = view_font_size()
     val size = change(size0) max font_size0 min font_size1
@@ -60,7 +60,7 @@
       jEdit.setIntegerProperty("view.fontsize", size)
       jEdit.propertiesChanged()
       jEdit.saveSettings()
-      view.getStatus.setMessageAndClear("Text font size: " + size)
+      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
     }
   }