src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Sat Nov 02 16:22:06 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Sat Nov 02 20:14:44 2024 +0100
@@ -12,8 +12,9 @@
 import java.awt.event.{KeyAdapter, KeyEvent, ItemListener, ItemEvent}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
+import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, JTree,
   RootPaneContainer, JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
+import javax.swing.tree.MutableTreeNode
 
 import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
   Orientation}
@@ -255,6 +256,15 @@
   }
 
 
+  /* tree view */
+
+  def init_tree(root: MutableTreeNode): JTree = {
+    val tree = new JTree(root)
+    tree.setRowHeight(0)
+    tree
+  }
+
+
   /* tooltip with multi-line support */
 
   def tooltip_lines(text: String): String =