--- 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)
}
}
}
--- 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 */