# HG changeset patch
# User wenzelm
# Date 1731507288 -3600
# Node ID 8d2d68c8c051c881b2cd49df5873b99ca629927e
# Parent  7436cdef0f145948947feb5d9480ff95094e4bcc
more ambitious mouse handler: double-click selects highlight_area;

diff -r 7436cdef0f14 -r 8d2d68c8c051 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Nov 13 14:54:08 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Nov 13 15:14:48 2024 +0100
@@ -23,7 +23,7 @@
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk, SyntaxStyle}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea, Selection}
 
 
 class Rich_Text_Area(
@@ -218,7 +218,8 @@
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
       robust_body(()) {
-        if (e.getClickCount == 1) {
+        val clicks = e.getClickCount
+        if (clicks == 1) {
           hyperlink_area.info match {
             case Some(Text.Info(range, link)) =>
               if (!link.external) {
@@ -241,6 +242,15 @@
             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 =>
+          }
+        }
       }
     }
   }