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