# HG changeset patch
# User wenzelm
# Date 1732009219 -3600
# Node ID a0ca6daf1ad6a45be9c9a82128146792d97f57d9
# Parent  3729744a08f38cd872e4257b2b9eb8253618e50d
re-use Output_Area with search results;

diff -r 3729744a08f3 -r a0ca6daf1ad6 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Nov 19 10:14:22 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Nov 19 10:40:19 2024 +0100
@@ -50,6 +50,9 @@
 
 
 class Info_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
+
   /* component state -- owned by GUI thread */
 
   private val snapshot = Info_Dockable.implicit_snapshot
@@ -65,47 +68,33 @@
     }
 
 
-  /* pretty text area */
-
-  private val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  /* output text area */
 
-  pretty_text_area.update(snapshot, results, info)
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-
-  /* resize */
+  private val output: Output_Area = new Output_Area(view)
+  output.pretty_text_area.update(snapshot, results, info)
 
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
+  private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components)
+  add(controls.peer, BorderLayout.NORTH)
 
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
-
-  add(controls.peer, BorderLayout.NORTH)
+  output.init_gui(dockable, split = true)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
-      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
+      case _: Session.Global_Options => GUI_Thread.later { output.handle_resize() }
     }
 
   override def init(): Unit = {
     GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main
-    handle_resize()
+    output.init()
   }
 
   override def exit(): Unit = {
     GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main
-    delay_resize.revoke()
+    output.exit()
   }
 }