# HG changeset patch
# User wenzelm
# Date 1732052898 -3600
# Node ID 57dc2c8ba7c6de7437d463eb254d1d4e747290dc
# Parent  b30dc7db521f17bec9246ba18b27c3ee4a4f998f
suppress odd icons for documents and folders;

diff -r b30dc7db521f -r 57dc2c8ba7c6 src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Tue Nov 19 22:41:57 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Tue Nov 19 22:48:18 2024 +0100
@@ -53,7 +53,9 @@
 
   /* cell renderer */
 
-  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = ()
+  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = {
+    renderer.setIcon(null)
+  }
 
   private val tree_cell_renderer: TreeCellRenderer = new DefaultTreeCellRenderer {
     override def getTreeCellRendererComponent(
diff -r b30dc7db521f -r 57dc2c8ba7c6 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 22:41:57 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 22:48:18 2024 +0100
@@ -37,7 +37,9 @@
         output_area.render_tree_cell(renderer)
     }
 
-  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = ()
+  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = {
+    renderer.setIcon(null)
+  }
 
   def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
     tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }