--- 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(
--- 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)) }