# HG changeset patch
# User wenzelm
# Date 1732009922 -3600
# Node ID 7293d47a9a70afd25bc34d792282a8838b6e0e32
# Parent  a0ca6daf1ad6a45be9c9a82128146792d97f57d9
re-use Output_Area with search results;

diff -r a0ca6daf1ad6 -r 7293d47a9a70 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Tue Nov 19 10:40:19 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Tue Nov 19 10:52:02 2024 +0100
@@ -19,28 +19,16 @@
   GUI_Thread.require {}
 
 
-  /* text area */
+  /* output text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  private val output: Output_Area = new Output_Area(view)
 
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
 
   private val print_state =
-    new Query_Operation(PIDE.editor, view, "print_state", _ => (), pretty_text_area.update)
-
-
-  /* resize */
+    new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update)
 
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
+  output.init_gui(this, split = true)
 
 
   /* update */
@@ -93,7 +81,7 @@
   private val controls =
     Wrap_Panel(
       List(auto_update_button, update_button, locate_button) :::
-      pretty_text_area.search_zoom_components)
+      output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -103,7 +91,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { handle_resize() }
+        GUI_Thread.later { output.handle_resize() }
 
       case changed: Session.Commands_Changed =>
         if (changed.assignment) GUI_Thread.later { auto_update() }
@@ -116,7 +104,7 @@
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
-    handle_resize()
+    output.init()
     print_state.activate()
     auto_update()
   }
@@ -126,6 +114,6 @@
     PIDE.session.caret_focus -= main
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
-    delay_resize.revoke()
+    output.exit()
   }
 }