# 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 = {