# HG changeset patch
# User wenzelm
# Date 1731579131 -3600
# Node ID cd685e2291faa02cd8bb9de2574cbb73aa34f95f
# Parent  7f3416f35b5dff05533fed7a4daf22f2ddfbfa09
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);

diff -r 7f3416f35b5d -r cd685e2291fa NEWS
--- a/NEWS	Thu Nov 14 10:50:49 2024 +0100
+++ b/NEWS	Thu Nov 14 11:12:11 2024 +0100
@@ -137,10 +137,12 @@
     with less load on the GUI thread.
 
   - Highlighting works via mouse hovering alone, without requiring
-    C-modifier. Double click selects that area.
+    C-modifier.
 
 * An active highlight area in the input buffer or output panel may be
-selected via double-click.
+turned into a text selection by using the ALT modifier. Together with
+SHIFT modifier, an existing selection is augmented (otherwise it is
+reset).
 
 * The "Documentation" panel supports plain text files again, notably
 "jedit-changes". This was broken in Isabelle2022, Isabelle2023,
diff -r 7f3416f35b5d -r cd685e2291fa src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Nov 14 10:50:49 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Nov 14 11:12:11 2024 +0100
@@ -424,6 +424,9 @@
   def shift_modifier(evt: InputEvent): Boolean =
     (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0
 
+  def alt_modifier(evt: InputEvent): Boolean =
+    (evt.getModifiersEx & InputEvent.ALT_DOWN_MASK) != 0
+
   def modifier_string(evt: InputEvent): String =
     KeyEventTranslator.getModifierString(evt) match {
       case null => ""
diff -r 7f3416f35b5d -r cd685e2291fa src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 14 10:50:49 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 14 11:12:11 2024 +0100
@@ -218,39 +218,27 @@
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
       robust_body(()) {
-        if (!e.isConsumed()) {
-          val clicks = e.getClickCount
-          if (clicks == 1) {
-            hyperlink_area.info match {
-              case Some(Text.Info(range, link)) =>
-                if (!link.external) {
-                  try { text_area.moveCaretPosition(range.start) }
-                  catch {
-                    case _: ArrayIndexOutOfBoundsException =>
-                    case _: IllegalArgumentException =>
-                  }
-                  text_area.requestFocus()
+        if (!e.isConsumed() && e.getClickCount == 1) {
+          hyperlink_area.info match {
+            case Some(Text.Info(range, link)) =>
+              if (!link.external) {
+                try { text_area.moveCaretPosition(range.start) }
+                catch {
+                  case _: ArrayIndexOutOfBoundsException =>
+                  case _: IllegalArgumentException =>
                 }
-                link.follow(view)
-                e.consume()
-              case None =>
-            }
-            active_area.text_info match {
-              case Some((text, Text.Info(_, markup))) =>
-                Active.action(view, text, markup)
-                close_action()
-                e.consume()
-              case None =>
-            }
+                text_area.requestFocus()
+              }
+              link.follow(view)
+              e.consume()
+            case None =>
           }
-          else if (clicks == 2) {
-            highlight_area.info match {
-              case Some(Text.Info(r, _)) =>
-                text_area.selectNone()
-                text_area.addToSelection(new Selection.Range(r.start, r.stop))
-                e.consume()
-              case None =>
-            }
+          active_area.text_info match {
+            case Some((text, Text.Info(_, markup))) =>
+              Active.action(view, text, markup)
+              close_action()
+              e.consume()
+            case None =>
           }
         }
       }
@@ -294,6 +282,14 @@
                   }
                   else area.reset()
                 }
+                if (JEdit_Lib.alt_modifier(evt)) {
+                  highlight_area.info.map(_.range) match {
+                    case Some(range) =>
+                      if (!JEdit_Lib.shift_modifier(evt)) text_area.selectNone()
+                      text_area.addToSelection(new Selection.Range(range.start, range.stop))
+                    case None =>
+                  }
+                }
             }
           }
         }