# HG changeset patch
# User wenzelm
# Date 1730105008 -3600
# Node ID 59994f7feace8427acfcb32cd1211f57c94f0ed8
# Parent  66c253421be4bc1a890c120ce680c55ced2d5cc1
GUI option "editor_auto_hovering" for Output panel;

diff -r 66c253421be4 -r 59994f7feace etc/options
--- a/etc/options	Mon Oct 28 09:40:28 2024 +0100
+++ b/etc/options	Mon Oct 28 09:43:28 2024 +0100
@@ -309,6 +309,9 @@
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
+public option editor_auto_hovering : bool = true
+  -- "automatic mouse hovering without keyboard modifier"
+
 public option editor_document_session : string = ""
   -- "session for interactive document preparation"
 
diff -r 66c253421be4 -r 59994f7feace src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Oct 28 09:40:28 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Oct 28 09:43:28 2024 +0100
@@ -73,6 +73,11 @@
     }
   }
 
+  object auto_hovering extends Bool_Access("editor_auto_hovering") {
+    class GUI extends Bool_GUI(this, "Auto hovering") {
+      tooltip = "Automatic mouse hovering without keyboard modifier"
+    }
+  }
 
 
   /* editor pane for plugin options */
diff -r 66c253421be4 -r 59994f7feace src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Oct 28 09:40:28 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Oct 28 09:43:28 2024 +0100
@@ -63,6 +63,8 @@
 
   private val output_state_button = new JEdit_Options.output_state.GUI
 
+  private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
   private val auto_update_button = new GUI.Check("Auto update", init = do_update) {
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
@@ -80,7 +82,7 @@
 
   private val controls =
     Wrap_Panel(
-      List(output_state_button, auto_update_button,
+      List(output_state_button, auto_hovering_button, auto_update_button,
         update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
 
   add(controls.peer, BorderLayout.NORTH)
@@ -94,6 +96,7 @@
         GUI_Thread.later {
           handle_resize()
           output_state_button.load()
+          auto_hovering_button.load()
           handle_update(do_update, None)
         }
 
diff -r 66c253421be4 -r 59994f7feace src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Oct 28 09:40:28 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Oct 28 09:43:28 2024 +0100
@@ -147,8 +147,8 @@
 
   private class Active_Area[A](
     render: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
-    val require_control: Boolean = false,
-    val ignore_control: Boolean = false,
+    require_control: => Boolean = false,
+    ignore_control: => Boolean = false,
     cursor: Int = -1
   ) {
     private var the_text_info: Option[(String, Text.Info[A])] = None
@@ -192,7 +192,8 @@
   // owned by GUI thread
 
   private val highlight_area =
-    new Active_Area[Color](_.highlight, ignore_control = true)
+    new Active_Area[Color](_.highlight, require_control = true,
+      ignore_control = JEdit_Options.auto_hovering())
 
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink](