--- 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
}