clarified signature;

--- a/src/Pure/GUI/gui.scala	Sat Nov 02 20:14:44 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Sat Nov 02 20:24:53 2024 +0100
@@ -14,7 +14,7 @@
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, JTree,
   RootPaneContainer, JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
-import javax.swing.tree.MutableTreeNode
+import javax.swing.tree.{MutableTreeNode, TreeSelectionModel}
 
 import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
   Orientation}
@@ -258,9 +258,14 @@
 
   /* tree view */
 
-  def init_tree(root: MutableTreeNode): JTree = {
+  def init_tree(root: MutableTreeNode, single_selection_mode: Boolean = false): JTree = {
     val tree = new JTree(root)
     tree.setRowHeight(0)
+
+    if (single_selection_mode) {
+      tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+    }
+
     tree
   }
 

--- a/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:14:44 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:24:53 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.{Dimension, Rectangle}
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.JTree
-import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel, TreePath}
+import javax.swing.tree.{DefaultMutableTreeNode, TreePath}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
 
 import scala.util.matching.Regex

--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Nov 02 20:14:44 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Nov 02 20:24:53 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.Dimension
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.JScrollPane
-import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
+import javax.swing.tree.DefaultMutableTreeNode
 
 import org.gjt.sp.jedit.{View, OperatingSystem}
 
@@ -39,8 +39,7 @@
       })
   }
 
-  private val tree = GUI.init_tree(root)
-  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+  private val tree = GUI.init_tree(root, single_selection_mode = true)
 
   override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
 

--- a/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 20:14:44 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sat Nov 02 20:24:53 2024 +0100
@@ -13,7 +13,7 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
 import javax.swing.{JTree, JComponent}
-import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
+import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel}
 import javax.swing.event.TreeSelectionEvent
 
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -29,7 +29,7 @@
   /* tree view */
 
   val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
-  val tree: JTree = GUI.init_tree(root)
+  val tree: JTree = GUI.init_tree(root, single_selection_mode = true)
 
   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.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
   tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))