# HG changeset patch
# User wenzelm
# Date 1732052517 -3600
# Node ID b30dc7db521f17bec9246ba18b27c3ee4a4f998f
# Parent  07e79b80e96d12f58715e526ed7c82df7b9b93c1
support for modified tree cell renderer;

diff -r 07e79b80e96d -r b30dc7db521f src/Pure/GUI/tree_view.scala
--- a/src/Pure/GUI/tree_view.scala	Tue Nov 19 15:46:22 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Tue Nov 19 22:41:57 2024 +0100
@@ -8,7 +8,7 @@
 
 import javax.swing.JTree
 import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel,
-  TreeSelectionModel}
+  TreeSelectionModel, TreeCellRenderer, DefaultTreeCellRenderer}
 
 
 object Tree_View {
@@ -51,8 +51,31 @@
     }
 
 
+  /* cell renderer */
+
+  def render_tree_cell(renderer: DefaultTreeCellRenderer): Unit = ()
+
+  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)
+
   setRowHeight(0)
 
   if (single_selection_mode) {
diff -r 07e79b80e96d -r b30dc7db521f src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 15:46:22 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Tue Nov 19 22:41:57 2024 +0100
@@ -14,6 +14,7 @@
   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,7 +32,12 @@
   /* tree view */
 
   val tree: Tree_View =
-    new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
+    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 = ()
 
   def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
     tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }