--- 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 =
--- 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 =
--- 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
--- 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))