# HG changeset patch
# User wenzelm
# Date 1731506048 -3600
# Node ID 7436cdef0f145948947feb5d9480ff95094e4bcc
# Parent  839c4b2b01fa83bbb34556771de018e527a7f0c9
more accurate mouse handler: only for single clicks, consume accepted event;

diff -r 839c4b2b01fa -r 7436cdef0f14 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Nov 13 11:53:02 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Nov 13 14:54:08 2024 +0100
@@ -218,24 +218,28 @@
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
       robust_body(()) {
-        hyperlink_area.info match {
-          case Some(Text.Info(range, link)) =>
-            if (!link.external) {
-              try { text_area.moveCaretPosition(range.start) }
-              catch {
-                case _: ArrayIndexOutOfBoundsException =>
-                case _: IllegalArgumentException =>
+        if (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 =>
+                }
+                text_area.requestFocus()
               }
-              text_area.requestFocus()
-            }
-            link.follow(view)
-          case None =>
-        }
-        active_area.text_info match {
-          case Some((text, Text.Info(_, markup))) =>
-            Active.action(view, text, markup)
-            close_action()
-          case None =>
+              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 =>
+          }
         }
       }
     }