# HG changeset patch
# User wenzelm
# Date 1730982179 -3600
# Node ID c677755779f50db4f4f05414d40d480c3916765c
# Parent  bcd880130390d745776ad9052328caec3f5178d5
more uniform pretty_text_area.zoom via its zoom_component;

diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -68,8 +68,6 @@
 
   private val output: Output_Area =
     new Output_Area(view, root_name = "Threads", split = true) {
-      override def handle_resize(): Unit = pretty_text_area.zoom(zoom)
-
       override def handle_update(): Unit = {
         val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
         val (new_threads, new_output) = debugger.status(tree_selection())
@@ -231,17 +229,13 @@
     tooltip = "Official Standard ML instead of Isabelle/ML"
   }
 
-  private val zoom =
-    new Font_Info.Zoom { override def changed(): Unit = output.handle_resize() }
-
   private val controls =
     Wrap_Panel(
       List(
         break_button, continue_button, step_button, step_over_button, step_out_button,
         context_label, Component.wrap(context_field),
         expression_label, Component.wrap(expression_field), eval_button, sml_button) :::
-      output.pretty_text_area.search_components :::
-      List(output.pretty_text_area.search_field, zoom))
+      output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -91,8 +91,7 @@
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-  private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) }
+  private def handle_resize(): Unit = pretty_text_area.zoom()
 
   private val delay_resize: Delay =
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
@@ -352,7 +351,7 @@
       override def clicked(): Unit = cancel_process()
     }
 
-  private val output_controls = Wrap_Panel(List(cancel_button, zoom))
+  private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -72,10 +72,7 @@
 
   pretty_text_area.update(snapshot, results, info)
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
-  private def handle_resize(): Unit =
-    GUI_Thread.require { pretty_text_area.zoom(zoom) }
+  private def handle_resize(): Unit = pretty_text_area.zoom()
 
 
   /* resize */
@@ -88,7 +85,7 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
+  private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -37,7 +37,7 @@
 
   val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
 
-  def handle_resize(): Unit = ()
+  def handle_resize(): Unit = pretty_text_area.zoom()
   def handle_update(): Unit = ()
 
   lazy val delay_resize: Delay =
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -30,8 +30,7 @@
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
 
-  private def handle_resize(): Unit =
-    GUI_Thread.require { pretty_text_area.zoom(zoom) }
+  private def handle_resize(): Unit = pretty_text_area.zoom()
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
     GUI_Thread.require {}
@@ -78,12 +77,10 @@
     override def clicked(): Unit = handle_update(true, None)
   }
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
   private val controls =
     Wrap_Panel(
       List(output_state_button, auto_hovering_button, auto_update_button, update_button) :::
-      pretty_text_area.search_components ::: List(zoom))
+      pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -120,9 +120,6 @@
     refresh()
   }
 
-  def zoom(zoom: GUI.Zoom): Unit =
-    resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))
-
   def update(
     base_snapshot: Document.Snapshot,
     base_results: Command.Results,
@@ -146,7 +143,7 @@
     if (current_body.isEmpty) None else Some(() => detach())
 
 
-  /* common GUI components */
+  /* search */
 
   val search_label: Component = new Label("Search:") {
     tooltip = "Search and highlight output via regular expression"
@@ -166,8 +163,6 @@
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     })
 
-  def search_components: List[Component] = List(search_label, search_field)
-
   private val search_field_foreground = search_field.foreground
 
   private def search_action(text_field: JTextField): Unit = {
@@ -188,6 +183,22 @@
   }
 
 
+  /* zoom */
+
+  val zoom_component: GUI.Zoom =
+    new Font_Info.Zoom { override def changed(): Unit = zoom() }
+
+  def zoom(zoom: GUI.Zoom = zoom_component): Unit =
+    resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))
+
+
+  /* common GUI components */
+
+  def search_components: List[Component] = List(search_label, search_field)
+
+  def search_zoom_components: List[Component] = List(search_label, search_field, zoom_component)
+
+
   /* key handling */
 
   override def getInputMethodRequests: InputMethodRequests = null
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -300,7 +300,7 @@
 
   private def handle_resize(): Unit =
     GUI_Thread.require {
-      if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom))
+      if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom = zoom))
     }
 
   private val delay_resize =
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -61,11 +61,7 @@
     new Simplifier_Trace_Window(view, current_snapshot, trace)
   }
 
-  private def handle_resize(): Unit = {
-    GUI_Thread.later {
-      text_area.resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale")))
-    }
-  }
+  private def handle_resize(): Unit = text_area.zoom()
 
   private def handle_update(follow: Boolean): Unit = {
     val (new_snapshot, new_command, new_results, new_id) =
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -130,7 +130,6 @@
   GUI_Thread.require {}
 
   private val pretty_text_area = new Pretty_Text_Area(view)
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
 
   size = new Dimension(500, 500)
   contents = new BorderPanel {
@@ -155,8 +154,7 @@
     pretty_text_area.update(snapshot, Command.Results.empty, xml)
   }
 
-  def handle_resize(): Unit =
-    GUI_Thread.later { pretty_text_area.zoom(zoom) }
+  def handle_resize(): Unit = pretty_text_area.zoom()
 
 
   /* resize */
@@ -172,7 +170,7 @@
 
   /* controls */
 
-  private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
+  private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
 
   peer.add(controls.peer, BorderLayout.NORTH)
 }
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -61,8 +61,7 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  private def handle_resize(): Unit =
-    GUI_Thread.require { pretty_text_area.zoom(zoom) }
+  private def handle_resize(): Unit = pretty_text_area.zoom()
 
 
   /* controls */
@@ -122,12 +121,11 @@
     override def clicked(): Unit = sledgehammer.locate_query()
   }
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
   private val controls =
     Wrap_Panel(
       List(provers_label, Component.wrap(provers), isar_proofs, try0,
-        process_indicator.component, apply_query, cancel_query, locate_query, zoom))
+        process_indicator.component, apply_query, cancel_query, locate_query,
+        pretty_text_area.zoom_component))
 
   add(controls.peer, BorderLayout.NORTH)
 
diff -r bcd880130390 -r c677755779f5 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Thu Nov 07 13:22:59 2024 +0100
@@ -42,8 +42,7 @@
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
-  private def handle_resize(): Unit =
-    GUI_Thread.require { pretty_text_area.zoom(zoom) }
+  private def handle_resize(): Unit = pretty_text_area.zoom()
 
 
   /* update */
@@ -93,12 +92,10 @@
     override def clicked(): Unit = print_state.locate_query()
   }
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
   private val controls =
     Wrap_Panel(
       List(auto_update_button, update_button, locate_button) :::
-      pretty_text_area.search_components ::: List(zoom))
+      pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)