changeset 49701 | e2762f962042 |
parent 49647 | 21ae8500d261 |
child 49726 | 2074197dc274 |
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Oct 04 18:28:31 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Oct 04 19:31:50 2012 +0200 @@ -48,7 +48,7 @@ Swing_Thread.require() pretty_text_area.resize(Isabelle.font_family(), - scala.math.round(Isabelle.font_size() * zoom_factor / 100)) + scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100)) } private def handle_update(follow: Boolean, restriction: Option[Set[Command]])