diff -r 9f509bc10a63 -r 508a673c87ac src/Pure/GUI/tree_view.scala --- a/src/Pure/GUI/tree_view.scala Tue Feb 11 23:31:12 2025 +0100 +++ b/src/Pure/GUI/tree_view.scala Wed Feb 12 00:40:57 2025 +0100 @@ -8,7 +8,7 @@ import javax.swing.JTree import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel, - TreeSelectionModel, TreeCellRenderer, DefaultTreeCellRenderer} + TreeSelectionModel, DefaultTreeCellRenderer} object Tree_View {