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