# HG changeset patch
# User wenzelm
# Date 1660298789 -7200
# Node ID d6e8d12494beef36c24cd7acddf192da45e2f49d
# Parent  74d6d09e1a363a8d90af651f0606073f5b3a34b2
clarified signature;

diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -72,12 +72,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(): Unit = {
     GUI_Thread.require {}
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -74,12 +74,8 @@
 
   private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
 
-  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) }
 
 
   /* resize */
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/output_dockable.scala
--- 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 {}
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -122,6 +122,9 @@
     refresh()
   }
 
+  def zoom(factor: Int): Unit =
+    resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100))
+
   def update(
     base_snapshot: Document.Snapshot,
     base_results: Command.Results,
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -302,12 +302,7 @@
   /* resize */
 
   private def handle_resize(): Unit =
-    GUI_Thread.require {
-      for (op <- operations) {
-        op.pretty_text_area.resize(
-          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
-      }
-    }
+    GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom.factor)) }
 
   private val delay_resize =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -158,12 +158,8 @@
     pretty_text_area.update(snapshot, Command.Results.empty, xml)
   }
 
-  def do_paint(): Unit = {
-    GUI_Thread.later {
-      pretty_text_area.resize(
-        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
-    }
-  }
+  def do_paint(): Unit =
+    GUI_Thread.later { pretty_text_area.zoom(zoom.factor) }
 
   def handle_resize(): Unit = do_paint()
 
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -62,12 +62,8 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  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) }
 
 
   /* controls */
diff -r 74d6d09e1a36 -r d6e8d12494be src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 11:47:41 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
@@ -45,12 +45,8 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  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) }
 
 
   /* update */