# HG changeset patch
# User wenzelm
# Date 1732007477 -3600
# Node ID 6ca7c8f56396c436ee20caecec996fdab2d69564
# Parent  f02d3e52a7d5c5c2d17f65c24222c8f02e8419df
unused;

diff -r f02d3e52a7d5 -r 6ca7c8f56396 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Mon Nov 18 16:48:11 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Tue Nov 19 10:11:17 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.{Dimension, Rectangle}
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.tree.TreePath
-import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
+import javax.swing.event.{DocumentListener, DocumentEvent}
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, Action}