changeset 50146 | 03f38212442a |
parent 50117 | 32755e357a51 |
child 50205 | 788c8263e634 |
--- 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]])