# HG changeset patch
# User wenzelm
# Date 1730659110 -3600
# Node ID 33fbf90fbc1df258f450411bff73baf8540e72cd
# Parent  0521e65af41eb8ffecf6e299dc1e4c2f42720fb7
clarified signature: more explicit types;

diff -r 0521e65af41e -r 33fbf90fbc1d etc/build.props
--- a/etc/build.props	Sun Nov 03 14:11:01 2024 +0100
+++ b/etc/build.props	Sun Nov 03 19:38:30 2024 +0100
@@ -81,6 +81,7 @@
   src/Pure/GUI/gui.scala \
   src/Pure/GUI/gui_thread.scala \
   src/Pure/GUI/popup.scala \
+  src/Pure/GUI/tree_view.scala \
   src/Pure/GUI/wrap_panel.scala \
   src/Pure/General/antiquote.scala \
   src/Pure/General/base64.scala \
diff -r 0521e65af41e -r 33fbf90fbc1d src/Pure/GUI/gui.scala
--- 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 =
diff -r 0521e65af41e -r 33fbf90fbc1d src/Pure/GUI/tree_view.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/tree_view.scala	Sun Nov 03 19:38:30 2024 +0100
@@ -0,0 +1,26 @@
+/*  Title:      Pure/GUI/tree_view.scala
+    Author:     Makarius
+
+Tree view with adjusted defaults.
+*/
+
+package isabelle
+
+import javax.swing.JTree
+import javax.swing.tree.{MutableTreeNode, TreeSelectionModel}
+
+
+class Tree_View(root: MutableTreeNode, single_selection_mode: Boolean = false) extends JTree(root) {
+  tree =>
+
+  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")
+  }
+}
diff -r 0521e65af41e -r 33fbf90fbc1d src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sun Nov 03 19:38:30 2024 +0100
@@ -11,7 +11,6 @@
 
 import java.awt.{Dimension, Rectangle}
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
-import javax.swing.JTree
 import javax.swing.tree.{DefaultMutableTreeNode, TreePath}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
 
@@ -67,7 +66,7 @@
   private var nodes = List.empty[Graph_Display.Node]
   private val root = new DefaultMutableTreeNode("Nodes")
 
-  val tree: JTree = GUI.init_tree(root)
+  val tree: Tree_View = new Tree_View(root)
 
   tree.addKeyListener(new KeyAdapter {
     override def keyPressed(e: KeyEvent): Unit =
diff -r 0521e65af41e -r 33fbf90fbc1d src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sun Nov 03 19:38:30 2024 +0100
@@ -11,7 +11,7 @@
 
 import java.awt.BorderLayout
 import java.awt.event.KeyEvent
-import javax.swing.{JTree, JMenuItem}
+import javax.swing.JMenuItem
 import javax.swing.tree.DefaultMutableTreeNode
 import javax.swing.event.TreeSelectionEvent
 
@@ -102,7 +102,7 @@
 
   /* tree view */
 
-  private def tree: JTree = tree_text_area.tree
+  private def tree: Tree_View = tree_text_area.tree
 
   private def tree_selection(): Option[Debugger.Context] =
     tree_text_area.get_tree_selection({ case c: Debugger.Context => c })
diff -r 0521e65af41e -r 33fbf90fbc1d src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sun Nov 03 19:38:30 2024 +0100
@@ -39,7 +39,7 @@
       })
   }
 
-  private val tree = GUI.init_tree(root, single_selection_mode = true)
+  private val tree = new Tree_View(root, single_selection_mode = true)
 
   override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
 
diff -r 0521e65af41e -r 33fbf90fbc1d src/Tools/jEdit/src/tree_text_area.scala
--- a/src/Tools/jEdit/src/tree_text_area.scala	Sun Nov 03 14:11:01 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala	Sun Nov 03 19:38:30 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.Dimension
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
-import javax.swing.{JTree, JComponent}
+import javax.swing.JComponent
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel}
 import javax.swing.event.TreeSelectionEvent
 
@@ -29,7 +29,7 @@
   /* tree view */
 
   val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
-  val tree: JTree = GUI.init_tree(root, single_selection_mode = true)
+  val tree: Tree_View = new Tree_View(root, single_selection_mode = true)
 
   def get_tree_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
     tree.getLastSelectedPathComponent match {