changeset 82142 | 508a673c87ac |
parent 81497 | da807cf1e461 |
child 82554 | fa069e15c8da |
--- 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 {