src/Tools/Graphview/tree_panel.scala
changeset 81320 f0fccb521124
parent 81319 a0b25f94c74a
child 81321 301feaa85406
--- a/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:14:44 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:24:53 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.{Dimension, Rectangle}
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.JTree
-import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel, TreePath}
+import javax.swing.tree.{DefaultMutableTreeNode, TreePath}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
 
 import scala.util.matching.Regex