diff -r 57dc2c8ba7c6 -r 76f360c63dfe src/Pure/GUI/tree_view.scala
--- 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(