more ambitious rendering: highlight active area for mouse hovering without modifier;

--- a/src/Tools/jEdit/src/document_view.scala	Wed Oct 16 23:13:02 2024 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 18 11:32:10 2024 +0200
@@ -68,7 +68,7 @@
   val rich_text_area: Rich_Text_Area =
     new Rich_Text_Area(text_area.getView, text_area,
       () => Document_View.rendering(doc_view), () => (), () => None,
-      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
+      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = true)
 
 
   /* perspective */

--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Oct 16 23:13:02 2024 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 18 11:32:10 2024 +0200
@@ -148,10 +148,14 @@
   private class Active_Area[A](
     render: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
     val require_control: Boolean = false,
+    val ignore_control: Boolean = false,
     cursor: Int = -1
   ) {
     private var the_text_info: Option[(String, Text.Info[A])] = None
 
+    def check_control(control: Boolean): Boolean =
+      control == require_control || ignore_control
+
     def is_active: Boolean = the_text_info.isDefined
     def text_info: Option[(String, Text.Info[A])] = the_text_info
     def info: Option[Text.Info[A]] = the_text_info.map(_._2)
@@ -188,7 +192,7 @@
   // owned by GUI thread
 
   private val highlight_area =
-    new Active_Area[Color](_.highlight, require_control = true)
+    new Active_Area[Color](_.highlight, ignore_control = true)
 
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink](
@@ -268,7 +272,7 @@
               case Some(range) =>
                 val rendering = get_rendering()
                 for (area <- active_areas) {
-                  if (control == area.require_control && !rendering.snapshot.is_outdated) {
+                  if (area.check_control(control) && !rendering.snapshot.is_outdated) {
                     area.update_rendering(rendering, range)
                   }
                   else area.reset()