--- a/src/Pure/GUI/tree_view.scala Tue Nov 19 22:48:18 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala Tue Nov 19 22:55:09 2024 +0100
@@ -24,6 +24,10 @@
case _ => None
}
}
+
+ def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = {
+ renderer.setIcon(null)
+ }
}
class Tree_View(
@@ -53,9 +57,8 @@
/* cell renderer */
- def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = {
- renderer.setIcon(null)
- }
+ def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit =
+ Tree_View.render_tree_cell(renderer)
private val tree_cell_renderer: TreeCellRenderer = new DefaultTreeCellRenderer {
override def getTreeCellRendererComponent(