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))
       }
   })