src/Pure/GUI/tree_view.scala

--- a/src/Pure/GUI/tree_view.scala	Sun Nov 03 20:00:54 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Sun Nov 03 20:01:26 2024 +0100
@@ -7,20 +7,41 @@
 package isabelle
 
 import javax.swing.JTree
-import javax.swing.tree.{MutableTreeNode, TreeSelectionModel}
+import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 
 
-class Tree_View(root: MutableTreeNode, single_selection_mode: Boolean = false) extends JTree(root) {
-  tree =>
+class Tree_View(
+  val root: DefaultMutableTreeNode = new DefaultMutableTreeNode,
+  single_selection_mode: Boolean = false
+) extends JTree(root) {
+  def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
+    getLastSelectedPathComponent match {
+      case node: DefaultMutableTreeNode =>
+        val obj = node.getUserObject
+        if (obj != null && which.isDefinedAt(obj)) Some(which(obj))
+        else None
+      case _ => None
+    }
 
-  tree.setRowHeight(0)
+  def clear(): Unit = {
+    clearSelection()
+    root.removeAllChildren()
+  }
+
+  def reload_model(): Unit =
+    getModel.asInstanceOf[DefaultTreeModel].reload(root)
+
+
+  /* init */
+
+  setRowHeight(0)
 
   if (single_selection_mode) {
-    tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+    getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
   }
 
   // follow jEdit
   if (!GUI.is_macos_laf) {
-    tree.putClientProperty("JTree.lineStyle", "Angled")
+    putClientProperty("JTree.lineStyle", "Angled")
   }
 }