--- 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))