--- 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) {