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