--- a/src/Tools/jEdit/src/info_dockable.scala Tue Dec 17 13:14:55 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Tue Dec 17 13:38:52 2024 +0100
@@ -77,7 +77,10 @@
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)
@@ -88,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 = {
--- a/src/Tools/jEdit/src/state_dockable.scala Tue Dec 17 13:14:55 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Dec 17 13:38:52 2024 +0100
@@ -74,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()
@@ -86,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)
@@ -97,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() }