font size change with delay, to avoid GUI lagging behind user input;

--- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 15:58:47 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 16:34:30 2014 +0100
@@ -186,14 +186,39 @@
 
   /* font size */
 
-  def reset_font_size(view: View): Unit =
-    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
+  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 =>
+        {
+          var j = i
+          while (steps != 0 && j > 0) {
+            if (steps > 0)
+              { j += (j / 10) max 1; steps -= 1 }
+            else
+              { j -= (j / 10) max 1; steps += 1 }
+          }
+          steps = 0
+          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 increase_font_size(view: View): Unit =
-    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
+  def reset_font_size(view: View): Unit =
+  {
+    font_size.reset()
+    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
+  }
 
-  def decrease_font_size(view: View): Unit =
-    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
+  def increase_font_size(view: View): Unit = font_size.step(view, 1)
+  def decrease_font_size(view: View): Unit = font_size.step(view, -1)
 
 
   /* structured edits */

--- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 15:58:47 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 16:34:30 2014 +0100
@@ -54,11 +54,14 @@
 
   def font_size_change(view: View, change: Int => Int)
   {
-    val size = change(view_font_size()) max font_size0 min font_size1
-    jEdit.setIntegerProperty("view.fontsize", size)
-    jEdit.propertiesChanged()
-    jEdit.saveSettings()
-    view.getStatus.setMessageAndClear("Text font size: " + size)
+    val size0 = view_font_size()
+    val size = change(size0) max font_size0 min font_size1
+    if (size != size0) {
+      jEdit.setIntegerProperty("view.fontsize", size)
+      jEdit.propertiesChanged()
+      jEdit.saveSettings()
+      view.getStatus.setMessageAndClear("Text font size: " + size)
+    }
   }