# HG changeset patch
# User wenzelm
# Date 1393700101 -3600
# Node ID 8a881f83e206c68f5a96584ea71c62c1b3135fe8
# Parent  e56a52dd770a52abc6393e2bc2b28d18eace531e
clarified module structure;

diff -r e56a52dd770a -r 8a881f83e206 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:43:35 2014 +0100
+++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:55:01 2014 +0100
@@ -1,7 +1,7 @@
-/*  Title:      Tools/jEdit/src/jedit_font.scala
+/*  Title:      Tools/jEdit/src/font_info.scala
     Author:     Makarius
 
-Font information, derived from main view font.
+Font information, derived from main jEdit view font.
 */
 
 package isabelle.jedit
@@ -25,7 +25,7 @@
   def restrict_size(size: Float): Float = size max min_size min max_size
 
 
-  /* jEdit font */
+  /* main jEdit font */
 
   def main_family(): String = jEdit.getProperty("view.font")
 
@@ -35,15 +35,54 @@
   def main(scale: Double = 1.0): Font_Info =
     Font_Info(main_family(), main_size(scale))
 
-  def main_change(change: Float => Float)
+
+  /* incremental size change */
+
+  object main_change
   {
-    val size0 = main_size()
-    val size = restrict_size(change(size0)).round
-    if (size != size0) {
-      jEdit.setIntegerProperty("view.fontsize", size)
-      jEdit.propertiesChanged()
-      jEdit.saveSettings()
-      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+    private def change_size(change: Float => Float)
+    {
+      Swing_Thread.require()
+
+      val size0 = main_size()
+      val size = restrict_size(change(size0)).round
+      if (size != size0) {
+        jEdit.setIntegerProperty("view.fontsize", size)
+        jEdit.propertiesChanged()
+        jEdit.saveSettings()
+        jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+      }
+    }
+
+    // owned by Swing thread
+    private var steps = 0
+    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+    {
+      change_size(size =>
+        {
+          var i = size.round
+          while (steps != 0 && i > 0) {
+            if (steps > 0)
+              { i += (i / 10) max 1; steps -= 1 }
+            else
+              { i -= (i / 10) max 1; steps += 1 }
+          }
+          steps = 0
+          i.toFloat
+        })
+    }
+
+    def step(i: Int)
+    {
+      steps += i
+      delay.invoke()
+    }
+
+    def reset(size: Float)
+    {
+      delay.revoke()
+      steps = 0
+      change_size(_ => size)
     }
   }
 }
diff -r e56a52dd770a -r 8a881f83e206 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:43:35 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:55:01 2014 +0100
@@ -186,37 +186,11 @@
 
   /* font size */
 
-  private object font_size
-  {
-    // owned by Swing thread
-    private var steps = 0
-    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
-    {
-      Font_Info.main_change(size =>
-        {
-          var i = size.round
-          while (steps != 0 && i > 0) {
-            if (steps > 0)
-              { i += (i / 10) max 1; steps -= 1 }
-            else
-              { i -= (i / 10) max 1; steps += 1 }
-          }
-          steps = 0
-          i.toFloat
-        })
-    }
-    def step(i: Int) { steps += i; delay.invoke() }
-    def reset() { delay.revoke(); steps = 0 }
+  def reset_font_size() {
+    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
   }
-
-  def reset_font_size()
-  {
-    font_size.reset()
-    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
-  }
-
-  def increase_font_size() { font_size.step(1) }
-  def decrease_font_size() { font_size.step(-1) }
+  def increase_font_size() { Font_Info.main_change.step(1) }
+  def decrease_font_size() { Font_Info.main_change.step(-1) }
 
 
   /* structured edits */