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]])