# 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 \ S \ {}}" 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} \ ?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 \ {}" -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 \The powerdomain basis type is countable.\ -lemma pd_basis_countable: "\f::'a::bifinite pd_basis \ nat. inj f" +lemma pd_basis_countable: "\f::'a::bifinite pd_basis \ nat. inj f" (is "Ex ?P") proof - obtain g :: "'a compact_basis \ nat" where "inj g" using compact_basis.countable .. - hence image_g_eq: "\A B. g ` A = g ` B \ A = B" + hence image_g_eq: "g ` A = g ` B \ A = B" for A B by (rule inj_image_eq_iff) have "inj (\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: "\a. P (PDUnit a)" assumes PDPlus: "\a t. P t \ 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 \ {}" 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: "\a. P (PDUnit a)" assumes PDPlus: "\t u. \P t; P u\ \ 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 \Fold operator\ 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 \\ ?v" "u \\ ?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: "\a b. a \ b \ P (PDUnit a) (PDUnit b)" assumes 4: "\t u v w. \P t v; P u w\ \ 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 \Type definition\ @@ -281,26 +285,34 @@ assumes unit: "\x. P {x}\" assumes insert: "\x ys. \P {x}\; P ys\ \ P ({x}\ \\ 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: "\x. P {x}\" assumes plus: "\xs ys. \P xs; P ys\ \ P (xs \\ 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 \Monadic bind\ 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: "\t u a. P (PDUnit a) t \ P (PDUnit a) (PDPlus t u)" assumes 3: "\t u v. \P t v; P u v\ \ 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 \\ t" | (u) "PDUnit a \\ 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 \Type definition\ @@ -271,29 +287,42 @@ lemma lower_pd_induct1: assumes P: "adm P" assumes unit: "\x. P {x}\" - assumes insert: - "\x ys. \P {x}\; P ys\ \ P ({x}\ \\ ys)" + assumes insert: "\x ys. \P {x}\; P ys\ \ P ({x}\ \\ 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}\" 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}\ \\ 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: "\x. P {x}\" assumes plus: "\xs ys. \P xs; P ys\ \ P (xs \\ 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 \Monadic bind\ 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: "\t u a. P t (PDUnit a) \ P (PDPlus t u) (PDUnit a)" assumes 3: "\t u v. \P t u; P t v\ \ 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 \\ PDUnit a" | (u) "u \\ 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 \Type definition\ @@ -267,26 +284,41 @@ assumes unit: "\x. P {x}\" assumes insert: "\x ys. \P {x}\; P ys\ \ P ({x}\ \\ 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}\" 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}\ \\ 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: "\x. P {x}\" assumes plus: "\xs ys. \P xs; P ys\ \ P (xs \\ 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 \Monadic bind\ 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 ++= ": " 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 ++= "" - s ++= line_text.substring(next, next + range.length) + s ++= plain_text.substring(next, next + range.length) s ++= "" 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 ++= "" } 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("Update") { 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() }