--- a/src/Pure/GUI/gui.scala Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Pure/GUI/gui.scala Sun Nov 03 19:38:30 2024 +0100
@@ -12,9 +12,8 @@
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, JTree,
+import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
RootPaneContainer, JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
-import javax.swing.tree.{MutableTreeNode, TreeSelectionModel}
import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
Orientation}
@@ -260,25 +259,6 @@
}
- /* tree view */
-
- 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)
- }
-
- // follow jEdit
- if (!GUI.is_macos_laf) {
- tree.putClientProperty("JTree.lineStyle", "Angled")
- }
-
- tree
- }
-
-
/* tooltip with multi-line support */
def tooltip_lines(text: String): String =