--- a/src/Tools/jEdit/src/output_dockable.scala Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Aug 12 12:06:29 2022 +0200
@@ -33,12 +33,8 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
GUI_Thread.require {}