src/Tools/Graphview/tree_panel.scala

--- a/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 16:22:06 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:14:44 2024 +0100
@@ -67,8 +67,7 @@
   private var nodes = List.empty[Graph_Display.Node]
   private val root = new DefaultMutableTreeNode("Nodes")
 
-  val tree = new JTree(root)
-  tree.setRowHeight(0)
+  val tree: JTree = GUI.init_tree(root)
 
   tree.addKeyListener(new KeyAdapter {
     override def keyPressed(e: KeyEvent): Unit =