diff -r a0b25f94c74a -r f0fccb521124 src/Tools/Graphview/tree_panel.scala --- 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