# HG changeset patch
# User wenzelm
# Date 1734435397 -3600
# Node ID ebf954ceb4d1193e05bab852d24c32ad81689dd0
# Parent  afd27db5a15bdd3e623487d25c2582de1bf82e8c
clarified split_pane layout: close on first display, open on first search;

diff -r afd27db5a15b -r ebf954ceb4d1 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Mon Dec 16 22:53:31 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Dec 17 12:36:37 2024 +0100
@@ -70,7 +70,11 @@
 
   /* output text area */
 
-  private val output: Output_Area = new Output_Area(view)
+  private val output: Output_Area =
+    new Output_Area(view) {
+      override def handle_shown(): Unit = split_pane_layout()
+    }
+
   output.pretty_text_area.update(snapshot, results, info)
 
   private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components)
diff -r afd27db5a15b -r ebf954ceb4d1 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Mon Dec 16 22:53:31 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Dec 17 12:36:37 2024 +0100
@@ -11,7 +11,7 @@
 
 import java.awt.Dimension
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
-  MouseEvent, MouseAdapter}
+  HierarchyListener, HierarchyEvent, MouseEvent, MouseAdapter}
 import javax.swing.{JComponent, JButton}
 import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
 
@@ -37,7 +37,13 @@
   val tree: Tree_View =
     new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
+  private var search_activated = false
+
   def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
+    if (!search_activated && search.pattern.isDefined) {
+      search_activated = true
+      delay_shown.invoke()
+    }
     tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
     tree.revalidate()
   }
@@ -67,6 +73,23 @@
   /* handle events */
 
   def handle_focus(): Unit = ()
+  def handle_shown(): Unit = ()
+
+  lazy val delay_shown: Delay =
+    Delay.first(PIDE.session.input_delay, gui = true) { handle_shown() }
+
+  private lazy val hierarchy_listener =
+    new HierarchyListener {
+      override def hierarchyChanged(e: HierarchyEvent): Unit = {
+        val displayed =
+          (e.getChangeFlags & HierarchyEvent.DISPLAYABILITY_CHANGED) != 0 &&
+            e.getComponent.isDisplayable
+        val shown =
+          (e.getChangeFlags & HierarchyEvent.SHOWING_CHANGED) != 0 &&
+            e.getComponent.isShowing
+        if (displayed || shown) delay_shown.invoke()
+      }
+    }
 
   private lazy val component_listener =
     new ComponentAdapter {
@@ -117,7 +140,7 @@
       rightComponent = text_pane
     }
 
-  def split_pane_layout(open: Boolean = false): Unit = {
+  def split_pane_layout(open: Boolean = search_activated): Unit = {
     split_pane.peer.getUI match {
       case ui: FlatSplitPaneUI =>
         val div = ui.getDivider
@@ -149,6 +172,7 @@
   }
 
   def setup(parent: JComponent): Unit = {
+    parent.addHierarchyListener(hierarchy_listener)
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
@@ -161,5 +185,8 @@
     handle_resize()
   }
 
-  def exit(): Unit = delay_resize.revoke()
+  def exit(): Unit = {
+    delay_resize.revoke()
+    delay_shown.revoke()
+  }
 }
diff -r afd27db5a15b -r ebf954ceb4d1 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Dec 16 22:53:31 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Dec 17 12:36:37 2024 +0100
@@ -27,8 +27,11 @@
 
   /* output area */
 
-  private val output: Output_Area =
-    new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) }
+  val output: Output_Area =
+    new Output_Area(view) {
+      override def handle_update(): Unit = dockable.handle_update(true)
+      override def handle_shown(): Unit = split_pane_layout()
+    }
 
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
diff -r afd27db5a15b -r ebf954ceb4d1 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Dec 16 22:53:31 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Tue Dec 17 12:36:37 2024 +0100
@@ -23,7 +23,10 @@
 
   /* output text area */
 
-  private val output: Output_Area = new Output_Area(view)
+  private val output: Output_Area =
+    new Output_Area(view) {
+      override def handle_shown(): Unit = split_pane_layout()
+    }
 
   override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation