# HG changeset patch
# User wenzelm
# Date 1730574884 -3600
# Node ID a0b25f94c74ab845176fd35f9c668d26a1723ac3
# Parent  f870d42c49463565489ae6c655cd4a7e756a7697
clarified signature;

diff -r f870d42c4946 -r a0b25f94c74a 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 =
diff -r f870d42c4946 -r a0b25f94c74a 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 =
diff -r f870d42c4946 -r a0b25f94c74a src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Nov 02 16:22:06 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Nov 02 20:14:44 2024 +0100
@@ -11,7 +11,7 @@
 
 import java.awt.Dimension
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JScrollPane}
+import javax.swing.JScrollPane
 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
 
 import org.gjt.sp.jedit.{View, OperatingSystem}
@@ -39,8 +39,7 @@
       })
   }
 
-  private val tree = new JTree(root)
-  tree.setRowHeight(0)
+  private val tree = GUI.init_tree(root)
   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
 
   override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
diff -r f870d42c4946 -r a0b25f94c74a src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 16:22:06 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 20:14:44 2024 +0100
@@ -29,7 +29,7 @@
   /* tree view */
 
   val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
-  val tree: JTree = new JTree(root)
+  val tree: JTree = GUI.init_tree(root)
 
   def get_tree_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
     tree.getLastSelectedPathComponent match {
@@ -50,7 +50,6 @@
   def reload(): Unit =
     tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
 
-  tree.setRowHeight(0)
   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
   tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))