src/Tools/jEdit/src/tree_text_area.scala
changeset 81329 1775fdc7274e
parent 81325 458e9e3b356e
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sun Nov 03 20:23:19 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sun Nov 03 20:53:12 2024 +0100
@@ -13,7 +13,6 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
-import javax.swing.tree.DefaultMutableTreeNode
 import javax.swing.event.TreeSelectionEvent
 
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -29,7 +28,7 @@
   /* tree view */
 
   val tree: Tree_View =
-    new Tree_View(root = new DefaultMutableTreeNode(root_name), single_selection_mode = true)
+    new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
   def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
   tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))