# HG changeset patch
# User wenzelm
# Date 1353503219 -3600
# Node ID 03f38212442a1cdd7508ed6c811dd4b5bc429cfb
# Parent  88ba14e563d4882e394ac54e41e70b88df29d674
tuned;

diff -r 88ba14e563d4 -r 03f38212442a src/Tools/jEdit/src/info_dockable.scala
--- 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)
   }
 
 
diff -r 88ba14e563d4 -r 03f38212442a src/Tools/jEdit/src/output_dockable.scala
--- 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]])
diff -r 88ba14e563d4 -r 03f38212442a src/Tools/jEdit/src/pretty_tooltip.scala
--- 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",
diff -r 88ba14e563d4 -r 03f38212442a src/Tools/jEdit/src/symbols_dockable.scala
--- 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)
   }