# HG changeset patch
# User wenzelm
# Date 1731577849 -3600
# Node ID 7f3416f35b5dff05533fed7a4daf22f2ddfbfa09
# Parent  6097eaaee6eee1e3dedd443429e27f82416fe5c0
more careful isConsumed() / consume() for key and mouse events;

diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -61,14 +61,15 @@
 
   tree.addKeyListener(new KeyAdapter {
     override def keyPressed(e: KeyEvent): Unit =
-      if (e.getKeyCode == KeyEvent.VK_ENTER) {
+      if (!e.isConsumed() && e.getKeyCode == KeyEvent.VK_ENTER) {
         e.consume()
         selection_action()
       }
   })
   tree.addMouseListener(new MouseAdapter {
     override def mousePressed(e: MouseEvent): Unit =
-      if (e.getClickCount == 2) {
+      if (!e.isConsumed() && e.getClickCount == 2) {
+        e.consume()
         point_action(tree.getPathForLocation(e.getX, e.getY))
       }
   })
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -629,8 +629,10 @@
 
   list_view.peer.addMouseListener(new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
-      if (complete_selected()) e.consume()
-      hide_popup()
+      if (!e.isConsumed()) {
+        if (complete_selected()) e.consume()
+        hide_popup()
+      }
     }
   })
 
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -49,11 +49,16 @@
   })
   tree.addMouseListener(new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
-      val click = tree.getPathForLocation(e.getX, e.getY)
-      if (click != null && e.getClickCount == 1) {
-        val click_node = click.getLastPathComponent
-        val path_node = tree.getLastSelectedPathComponent
-        if (click_node == path_node) action(click_node)
+      if (!e.isConsumed()) {
+        val click = tree.getPathForLocation(e.getX, e.getY)
+        if (click != null && e.getClickCount == 1) {
+          val click_node = click.getLastPathComponent
+          val path_node = tree.getLastSelectedPathComponent
+          if (click_node == path_node) {
+            e.consume()
+            action(click_node)
+          }
+        }
       }
     }
   })
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -85,8 +85,13 @@
     tree.addMouseListener(
       new MouseAdapter {
         override def mouseClicked(e: MouseEvent): Unit = {
-          val click = tree.getPathForLocation(e.getX, e.getY)
-          if (click != null && e.getClickCount == 1) handle_focus()
+          if (!e.isConsumed()) {
+            val click = tree.getPathForLocation(e.getX, e.getY)
+            if (click != null && e.getClickCount == 1) {
+              e.consume()
+              handle_focus()
+            }
+          }
         }
       })
 
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -218,37 +218,39 @@
   private val mouse_listener = new MouseAdapter {
     override def mouseClicked(e: MouseEvent): Unit = {
       robust_body(()) {
-        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 =>
+        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()
                 }
-                text_area.requestFocus()
-              }
-              link.follow(view)
-              e.consume()
-            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 =>
+            }
           }
-          active_area.text_info match {
-            case Some((text, Text.Info(_, markup))) =>
-              Active.action(view, text, markup)
-              close_action()
-              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 =>
+          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 =>
+            }
           }
         }
       }
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/status_widget.scala
--- a/src/Tools/jEdit/src/status_widget.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/status_widget.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -87,7 +87,8 @@
 
     addMouseListener(new MouseAdapter {
       override def mouseClicked(evt: MouseEvent): Unit = {
-        if (evt.getClickCount == 2) {
+        if (!evt.isConsumed() && evt.getClickCount == 2) {
+          evt.consume()
           view.getInputHandler.invokeAction(action)
         }
       }
diff -r 6097eaaee6ee -r 7f3416f35b5d src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Wed Nov 13 23:11:06 2024 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Nov 14 10:50:49 2024 +0100
@@ -33,9 +33,13 @@
 
   addMouseListener(new MouseAdapter {
     override def mousePressed(event: MouseEvent): Unit = {
-      val line = (event.getY * lines()) / getHeight
-      if (line >= 0 && line < text_area.getLineCount)
-        text_area.setCaretPosition(text_area.getLineStartOffset(line))
+      if (!event.isConsumed()) {
+        val line = (event.getY * lines()) / getHeight
+        if (line >= 0 && line < text_area.getLineCount) {
+          event.consume()
+          text_area.setCaretPosition(text_area.getLineStartOffset(line))
+        }
+      }
     }
   })