# HG changeset patch
# User wenzelm
# Date 1732189662 -3600
# Node ID da807cf1e461d4372693fd6961886737ed335f30
# Parent  76f360c63dfe692c76e7dcc08c005683a8a9110f
clarified signature and object initialization;

diff -r 76f360c63dfe -r da807cf1e461 src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Tue Nov 19 22:55:09 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Thu Nov 21 12:47:42 2024 +0100
@@ -25,8 +25,22 @@
       }
   }
 
-  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = {
-    renderer.setIcon(null)
+  class Cell_Renderer extends DefaultTreeCellRenderer {
+    def setup(value: AnyRef): Unit = setIcon(null)
+
+    override def getTreeCellRendererComponent(
+      tree: JTree,
+      value: AnyRef,
+      selected: Boolean,
+      expanded: Boolean,
+      leaf: Boolean,
+      row: Int,
+      hasFocus: Boolean
+    ): java.awt.Component = {
+      super.getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus)
+      setup(value)
+      this
+    }
   }
 }
 
@@ -55,31 +69,9 @@
     }
 
 
-  /* cell renderer */
-
-  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit =
-    Tree_View.render_tree_cell(renderer)
-
-  private val tree_cell_renderer: TreeCellRenderer = new DefaultTreeCellRenderer {
-    override def getTreeCellRendererComponent(
-      tree: JTree,
-      value: AnyRef,
-      selected: Boolean,
-      expanded: Boolean,
-      leaf: Boolean,
-      row: Int,
-      hasFocus: Boolean
-    ): java.awt.Component = {
-      super.getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus)
-      render_tree_cell(this)
-      this
-    }
-  }
-
-
   /* init */
 
-  setCellRenderer(tree_cell_renderer)
+  setCellRenderer(new Tree_View.Cell_Renderer)
 
   setRowHeight(0)
 
diff -r 76f360c63dfe -r da807cf1e461 src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 22:55:09 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Thu Nov 21 12:47:42 2024 +0100
@@ -14,7 +14,6 @@
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
 import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
-import javax.swing.tree.DefaultTreeCellRenderer
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -31,14 +30,10 @@
 
   /* tree view */
 
+  val tree_cell_renderer: Tree_View.Cell_Renderer = new Tree_View.Cell_Renderer
+
   val tree: Tree_View =
-    new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true) {
-      override def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit =
-        output_area.render_tree_cell(renderer)
-    }
-
-  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit =
-    Tree_View.render_tree_cell(renderer)
+    new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
   def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
     tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
@@ -125,6 +120,7 @@
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
     tree.addTreeSelectionListener(tree_selection_listener)
+    tree.setCellRenderer(tree_cell_renderer)
   }
 
   def init(): Unit = {