--- a/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 19:38:30 2024 +0100
@@ -12,7 +12,7 @@
import java.awt.Dimension
import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JComponent}
+import javax.swing.JComponent
import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel}
import javax.swing.event.TreeSelectionEvent
@@ -29,7 +29,7 @@
/* tree view */
val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
- val tree: JTree = GUI.init_tree(root, single_selection_mode = true)
+ val tree: Tree_View = new Tree_View(root, single_selection_mode = true)
def get_tree_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
tree.getLastSelectedPathComponent match {