equal
deleted
inserted
replaced
46 private def handle_resize() |
46 private def handle_resize() |
47 { |
47 { |
48 Swing_Thread.require() |
48 Swing_Thread.require() |
49 |
49 |
50 pretty_text_area.resize(Isabelle.font_family(), |
50 pretty_text_area.resize(Isabelle.font_family(), |
51 scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100)) |
51 (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round) |
52 } |
52 } |
53 |
53 |
54 private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) |
54 private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) |
55 { |
55 { |
56 Swing_Thread.require() |
56 Swing_Thread.require() |