# HG changeset patch
# User wenzelm
# Date 1734519584 -3600
# Node ID 91a7e5719b2b365241780cbaf306d7286319af72
# Parent  44afa6f1baad90d9e8878136aba4359e3e8653c8# Parent  f57732142e0d4338548e962040f719c0253cfaab
merged

diff -r 44afa6f1baad -r 91a7e5719b2b src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Wed Dec 18 11:59:44 2024 +0100
@@ -13,29 +13,28 @@
 definition "pd_basis = {S::'a::bifinite compact_basis set. finite S \<and> S \<noteq> {}}"
 
 typedef 'a::bifinite pd_basis = "pd_basis :: 'a compact_basis set set"
-  unfolding pd_basis_def
-  apply (rule_tac x="{_}" in exI)
-  apply simp
-  done
+proof
+  show "{a} \<in> ?pd_basis" for a
+    by (simp add: pd_basis_def)
+qed
 
 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+using Rep_pd_basis [of u, unfolded pd_basis_def] by simp
 
 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
-by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
+using Rep_pd_basis [of u, unfolded pd_basis_def] by simp
 
 text \<open>The powerdomain basis type is countable.\<close>
 
-lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f"
+lemma pd_basis_countable: "\<exists>f::'a::bifinite pd_basis \<Rightarrow> nat. inj f" (is "Ex ?P")
 proof -
   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
     using compact_basis.countable ..
-  hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B"
+  hence image_g_eq: "g ` A = g ` B \<longleftrightarrow> A = B" for A B
     by (rule inj_image_eq_iff)
   have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))"
     by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
-  thus ?thesis by - (rule exI)
-  (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
+  thus ?thesis by (rule exI [of ?P])
 qed
 
 
@@ -69,26 +68,30 @@
 lemma PDPlus_absorb: "PDPlus t t = t"
 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
 
-lemma pd_basis_induct1:
+lemma pd_basis_induct1 [case_names PDUnit PDPlus]:
   assumes PDUnit: "\<And>a. P (PDUnit a)"
   assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
   shows "P x"
-apply (induct x, unfold pd_basis_def, clarify)
-apply (erule (1) finite_ne_induct)
-apply (cut_tac a=x in PDUnit)
-apply (simp add: PDUnit_def)
-apply (drule_tac a=x in PDPlus)
-apply (simp add: PDUnit_def PDPlus_def
-  Abs_pd_basis_inverse [unfolded pd_basis_def])
-done
+proof (induct x)
+  case (Abs_pd_basis y)
+  then have "finite y" and "y \<noteq> {}" by (simp_all add: pd_basis_def)
+  then show ?case
+  proof (induct rule: finite_ne_induct)
+    case (singleton x)
+    show ?case by (rule PDUnit [unfolded PDUnit_def])
+  next
+    case (insert x F)
+    from insert(4) have "P (PDPlus (PDUnit x) (Abs_pd_basis F))" by (rule PDPlus)
+    with insert(1,2) show ?case
+      by (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
+  qed
+qed
 
-lemma pd_basis_induct:
+lemma pd_basis_induct [case_names PDUnit PDPlus]:
   assumes PDUnit: "\<And>a. P (PDUnit a)"
   assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
   shows "P x"
-apply (induct x rule: pd_basis_induct1)
-apply (rule PDUnit, erule PDPlus [OF PDUnit])
-done
+  by (induct x rule: pd_basis_induct1) (fact PDUnit, fact PDPlus [OF PDUnit])
 
 
 subsection \<open>Fold operator\<close>
diff -r 44afa6f1baad -r 91a7e5719b2b src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 18 11:59:44 2024 +0100
@@ -92,10 +92,7 @@
     apply fast
     done
   show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
-   apply (insert z)
-   apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
-   apply fast+
-   done
+    using z by (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w) fast+
 qed
 
 lemma convex_le_induct [induct set: convex_le]:
@@ -104,17 +101,24 @@
   assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
   assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
   shows "P t u"
-using le apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct1)
-apply (simp add: 3)
-apply (simp, clarify, rename_tac a b t)
-apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
-apply (simp add: PDPlus_absorb)
-apply (erule (1) 4 [OF 3])
-apply (drule convex_le_PDPlus_lemma, clarify)
-apply (simp add: 4)
-done
+  using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+  case (PDUnit a)
+  then show ?case
+  proof (induct u rule: pd_basis_induct1)
+    case (PDUnit b)
+    then show ?case by (simp add: 3)
+  next
+    case (PDPlus b t)
+    have "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)"
+      by (rule 4 [OF 3]) (use PDPlus in simp_all)
+    then show ?case by (simp add: PDPlus_absorb)
+  qed
+next
+  case PDPlus
+  from PDPlus(1,2) show ?case
+    using convex_le_PDPlus_lemma [OF PDPlus(3)] by (auto simp add: 4)
+qed
 
 
 subsection \<open>Type definition\<close>
@@ -281,26 +285,34 @@
   assumes unit: "\<And>x. P {x}\<natural>"
   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
   shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric]
-                  convex_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: convex_pd.principal_induct)
+  show "P (convex_principal a)" for a
+  proof (induct a rule: pd_basis_induct1)
+    case PDUnit
+    show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric]) (rule unit)
+  next
+    case PDPlus
+    show ?case
+      by (simp only: convex_unit_Rep_compact_basis [symmetric] convex_plus_principal [symmetric])
+        (rule insert [OF unit PDPlus])
+  qed
+qed (rule P)
 
-lemma convex_pd_induct
-  [case_names adm convex_unit convex_plus, induct type: convex_pd]:
+lemma convex_pd_induct [case_names adm convex_unit convex_plus, induct type: convex_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<natural>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
   shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: convex_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: convex_pd.principal_induct)
+  show "P (convex_principal a)" for a
+  proof (induct a rule: pd_basis_induct)
+    case PDUnit
+    then show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
+  next
+    case PDPlus
+    then show ?case by (simp only: convex_plus_principal [symmetric] plus)
+  qed
+qed (rule P)
 
 
 subsection \<open>Monadic bind\<close>
diff -r 44afa6f1baad -r 91a7e5719b2b src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 18 11:59:44 2024 +0100
@@ -59,17 +59,33 @@
   assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
   assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
   shows "P t u"
-using le
-apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: lower_le_PDUnit_PDPlus_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: lower_le_PDPlus_iff 3)
-done
+  using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+  case (PDUnit a)
+  then show ?case
+  proof (induct u rule: pd_basis_induct)
+    case PDUnit
+    then show ?case by (simp add: 1)
+  next
+    case (PDPlus t u)
+    from PDPlus(3) consider (t) "PDUnit a \<le>\<flat> t" | (u) "PDUnit a \<le>\<flat> u"
+      by (auto simp: lower_le_PDUnit_PDPlus_iff)
+    then show ?case
+    proof cases
+      case t
+      then have "P (PDUnit a) t" by (rule PDPlus(1))
+      then show ?thesis by (rule 2)
+    next
+      case u
+      then have "P (PDUnit a) u" by (rule PDPlus(2))
+      then have "P (PDUnit a) (PDPlus u t)" by (rule 2)
+      then show ?thesis by (simp only: PDPlus_commute)
+    qed
+  qed
+next
+  case (PDPlus t t')
+  then show ?case by (simp add: lower_le_PDPlus_iff 3)
+qed
 
 
 subsection \<open>Type definition\<close>
@@ -271,29 +287,42 @@
 lemma lower_pd_induct1:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
-  assumes insert:
-    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
+  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
   shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric]
-                  lower_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: lower_pd.principal_induct)
+  have *: "P {Rep_compact_basis a}\<flat>" for a
+    by (rule unit)
+  show "P (lower_principal a)" for a
+  proof (induct a rule: pd_basis_induct1)
+    case PDUnit
+    from * show ?case
+      by (simp only: lower_unit_Rep_compact_basis [symmetric])
+  next
+    case (PDPlus a t)
+    with * have "P ({Rep_compact_basis a}\<flat> \<union>\<flat> lower_principal t)"
+      by (rule insert)
+    then show ?case
+      by (simp only: lower_unit_Rep_compact_basis [symmetric] lower_plus_principal [symmetric])
+  qed
+qed (rule P)
 
-lemma lower_pd_induct
-  [case_names adm lower_unit lower_plus, induct type: lower_pd]:
+lemma lower_pd_induct [case_names adm lower_unit lower_plus, induct type: lower_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
   shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: lower_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: lower_pd.principal_induct)
+  show "P (lower_principal a)" for a
+  proof (induct a rule: pd_basis_induct)
+    case PDUnit
+    then show ?case
+      by (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
+  next
+    case PDPlus
+    then show ?case
+      by (simp only: lower_plus_principal [symmetric] plus)
+  qed
+qed (rule P)
 
 
 subsection \<open>Monadic bind\<close>
diff -r 44afa6f1baad -r 91a7e5719b2b src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 18 11:59:44 2024 +0100
@@ -58,16 +58,33 @@
   assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
   assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
   shows "P t u"
-using le apply (induct u arbitrary: t rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac t rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: upper_le_PDPlus_PDUnit_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: upper_le_PDPlus_iff 3)
-done
+  using le
+proof (induct u arbitrary: t rule: pd_basis_induct)
+  case (PDUnit a)
+  then show ?case
+  proof (induct t rule: pd_basis_induct)
+    case PDUnit
+    then show ?case by (simp add: 1)
+  next
+    case (PDPlus t u)
+    from PDPlus(3) consider (t) "t \<le>\<sharp> PDUnit a" | (u) "u \<le>\<sharp> PDUnit a"
+      by (auto simp: upper_le_PDPlus_PDUnit_iff)
+    then show ?case
+    proof cases
+      case t
+      then have "P t (PDUnit a)" by (rule PDPlus(1))
+      then show ?thesis by (rule 2)
+    next
+      case u
+      then have "P u (PDUnit a)" by (rule PDPlus(2))
+      then have "P (PDPlus u t) (PDUnit a)" by (rule 2)
+      then show ?thesis by (simp only: PDPlus_commute)
+    qed
+  qed
+next
+  case (PDPlus t t' u)
+  then show ?case by (simp add: upper_le_PDPlus_iff 3)
+qed
 
 
 subsection \<open>Type definition\<close>
@@ -267,26 +284,41 @@
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
   shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric]
-                  upper_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: upper_pd.principal_induct)
+  have *: "P {Rep_compact_basis a}\<sharp>" for a
+    by (rule unit)
+  show "P (upper_principal a)" for a
+  proof (induct a rule: pd_basis_induct1)
+    case (PDUnit a)
+    with * show ?case
+      by (simp only: upper_unit_Rep_compact_basis [symmetric])
+  next
+    case (PDPlus a t)
+    with * have "P ({Rep_compact_basis a}\<sharp> \<union>\<sharp> upper_principal t)"
+      by (rule insert)
+    then show ?case
+      by (simp only: upper_unit_Rep_compact_basis [symmetric]
+          upper_plus_principal [symmetric])
+  qed
+qed (rule P)
 
-lemma upper_pd_induct
-  [case_names adm upper_unit upper_plus, induct type: upper_pd]:
+lemma upper_pd_induct [case_names adm upper_unit upper_plus, induct type: upper_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
   shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: upper_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: upper_pd.principal_induct)
+  show "P (upper_principal a)" for a
+  proof (induct a rule: pd_basis_induct)
+    case PDUnit
+    then show ?case
+      by (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
+  next
+    case PDPlus
+    then show ?case
+      by (simp only: upper_plus_principal [symmetric] plus)
+  qed
+qed (rule P)
 
 
 subsection \<open>Monadic bind\<close>
diff -r 44afa6f1baad -r 91a7e5719b2b src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Dec 18 11:59:44 2024 +0100
@@ -70,10 +70,17 @@
 
   /* 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)
+  private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
+  private val controls =
+    Wrap_Panel(auto_hovering_button :: output.pretty_text_area.search_zoom_components)
   add(controls.peer, BorderLayout.NORTH)
 
   output.setup(dockable)
@@ -84,7 +91,11 @@
 
   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
-      case _: Session.Global_Options => GUI_Thread.later { output.handle_resize() }
+      case _: Session.Global_Options =>
+        GUI_Thread.later {
+          output.handle_resize()
+          auto_hovering_button.load()
+        }
     }
 
   override def init(): Unit = {
diff -r 44afa6f1baad -r 91a7e5719b2b src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Dec 18 11:59:44 2024 +0100
@@ -11,9 +11,10 @@
 
 import java.awt.Dimension
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
-  MouseEvent, MouseAdapter}
-import javax.swing.JComponent
+  HierarchyListener, HierarchyEvent, MouseEvent, MouseAdapter}
+import javax.swing.{JComponent, JButton}
 import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
+import javax.swing.plaf.basic.BasicSplitPaneUI
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -22,7 +23,7 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View, root_name: String = "Search results") {
+class Output_Area(view: View, root_name: String = Pretty_Text_Area.search_title()) {
   output_area =>
 
   GUI_Thread.require {}
@@ -35,8 +36,17 @@
   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 = {
-    tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
+    if (!search_activated && search.pattern.isDefined) {
+      search_activated = true
+      delay_shown.invoke()
+    }
+    tree.init_model {
+      tree.root.setUserObject(Pretty_Text_Area.search_title(lines = search.length))
+      for (result <- search.results) tree.root.add(Tree_View.Node(result))
+    }
     tree.revalidate()
   }
 
@@ -65,6 +75,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 {
@@ -115,7 +142,47 @@
       rightComponent = text_pane
     }
 
+  def split_pane_layout(open: Boolean = search_activated): Unit = {
+    split_pane.peer.getUI match {
+      case ui: BasicSplitPaneUI =>
+        val div = ui.getDivider
+
+        val orientation = split_pane.orientation
+        val location = split_pane.dividerLocation
+        val insets = split_pane.peer.getInsets
+
+        val (left_collapsed, right_collapsed) =
+          if (orientation == Orientation.Vertical) {
+            (location == insets.left,
+              location == (split_pane.peer.getWidth - div.getWidth - insets.right))
+          }
+          else {
+            (location == insets.top,
+              location == (split_pane.peer.getHeight - div.getHeight - insets.bottom))
+          }
+
+        def click(i: Int): Unit = {
+          val comp =
+            try { div.getComponent(i) }
+            catch { case _: ArrayIndexOutOfBoundsException => null }
+          comp match {
+            case button: JButton => button.doClick()
+            case _ =>
+          }
+        }
+
+        if (open && left_collapsed) click(1)
+        else if (open && right_collapsed || !open && !left_collapsed) click(0)
+        else if (!open && right_collapsed) {
+          click(0)
+          GUI_Thread.later { click(0) }  // FIXME!?
+        }
+      case _ =>
+    }
+  }
+
   def setup(parent: JComponent): Unit = {
+    parent.addHierarchyListener(hierarchy_listener)
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
@@ -128,5 +195,8 @@
     handle_resize()
   }
 
-  def exit(): Unit = delay_resize.revoke()
+  def exit(): Unit = {
+    delay_resize.revoke()
+    delay_shown.revoke()
+  }
 }
diff -r 44afa6f1baad -r 91a7e5719b2b src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Dec 18 11:59:44 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 44afa6f1baad -r 91a7e5719b2b src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Dec 18 11:59:44 2024 +0100
@@ -50,24 +50,28 @@
       s ++= ":</b> "
 
       val line_start = line_range.start
-      val search_range = Text.Range(line_start, line_start + line_text.length)
+      val plain_text = line_text.replace('\t',' ').trim
+      val search_range = Text.Range(line_start, line_start + plain_text.length)
       var last = 0
       for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
         val next = range.start - line_start
-        if (last < next) s ++= line_text.substring(last, next)
+        if (last < next) s ++= plain_text.substring(last, next)
         s ++= "<span style=\""
         s ++= highlight_style
         s ++= "\">"
-        s ++= line_text.substring(next, next + range.length)
+        s ++= plain_text.substring(next, next + range.length)
         s ++= "</span>"
         last = range.stop - line_start
       }
-      if (last < line_text.length) s ++= line_text.substring(last)
+      if (last < plain_text.length) s ++= plain_text.substring(last)
       s ++= "</html>"
     }
     override def toString: String = gui_text
   }
 
+  def search_title(lines: Int = 0): String =
+    "Search result" + (if (lines <= 1) "" else " (" + lines + " lines)")
+
   sealed case class Search_Results(
     buffer: JEditBuffer,
     highlight_style: String,
diff -r 44afa6f1baad -r 91a7e5719b2b src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Wed Dec 18 11:59:44 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
 
@@ -71,6 +74,8 @@
     }
   }
 
+  private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
   private val update_button = new GUI.Button("<html><b>Update</b></html>") {
     tooltip = "Update display according to the command at cursor position"
     override def clicked(): Unit = update_request()
@@ -83,7 +88,7 @@
 
   private val controls =
     Wrap_Panel(
-      List(auto_update_button, update_button, locate_button) :::
+      List(auto_hovering_button, auto_update_button, update_button, locate_button) :::
       output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
@@ -94,7 +99,10 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { output.handle_resize() }
+        GUI_Thread.later {
+          output.handle_resize()
+          auto_hovering_button.load()
+        }
 
       case changed: Session.Commands_Changed =>
         if (changed.assignment) GUI_Thread.later { auto_update() }