--- a/src/Tools/jEdit/src/info_dockable.scala Wed Nov 21 13:47:47 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed Nov 21 14:06:59 2012 +0100
@@ -77,7 +77,7 @@
Swing_Thread.require()
pretty_text_area.resize(Isabelle.font_family(),
- scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
+ (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Nov 21 13:47:47 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Nov 21 14:06:59 2012 +0100
@@ -48,7 +48,7 @@
Swing_Thread.require()
pretty_text_area.resize(Isabelle.font_family(),
- scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
+ (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Nov 21 13:47:47 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Nov 21 14:06:59 2012 +0100
@@ -68,8 +68,8 @@
val pretty_text_area = new Pretty_Text_Area(view)
pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
- pretty_text_area.resize(
- Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
+ pretty_text_area.resize(Isabelle.font_family(),
+ Isabelle.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, body)
pretty_text_area.registerKeyboardAction(action_listener, "close_all",
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 13:47:47 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 14:06:59 2012 +0100
@@ -30,7 +30,8 @@
{
val dec = Symbol.decode(symbol)
font =
- new Font(Isabelle.font_family(), Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
+ new Font(Isabelle.font_family(),
+ Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
tooltip = symbol + " - " + get_name(dec)
}