--- 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")
}
}
--- a/src/Tools/Graphview/tree_panel.scala Sun Nov 03 20:00:54 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Sun Nov 03 20:01:26 2024 +0100
@@ -64,9 +64,8 @@
/* tree */
private var nodes = List.empty[Graph_Display.Node]
- private val root = new DefaultMutableTreeNode("Nodes")
- val tree: Tree_View = new Tree_View(root)
+ val tree: Tree_View = new Tree_View(root = new DefaultMutableTreeNode("Nodes"))
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit =
@@ -153,8 +152,8 @@
nodes = new_nodes
- root.removeAllChildren
- for (node <- nodes) root.add(new DefaultMutableTreeNode(node))
+ tree.root.removeAllChildren
+ for (node <- nodes) tree.root.add(new DefaultMutableTreeNode(node))
tree.expandRow(0)
tree.revalidate()
--- a/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 03 20:00:54 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 03 20:01:26 2024 +0100
@@ -105,7 +105,7 @@
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 })
+ tree_text_area.tree.get_selection({ case c: Debugger.Context => c })
private def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
@@ -122,16 +122,16 @@
case _ => thread_contexts.headOption
}
- tree_text_area.clear()
+ tree_text_area.tree.clear()
for (thread <- thread_contexts) {
val thread_node = new DefaultMutableTreeNode(thread)
for ((_, i) <- thread.debug_states.zipWithIndex)
thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
- tree_text_area.root.add(thread_node)
+ tree_text_area.tree.root.add(thread_node)
}
- tree_text_area.reload()
+ tree_text_area.tree.reload_model()
tree.expandRow(0)
for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sun Nov 03 20:00:54 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sun Nov 03 20:01:26 2024 +0100
@@ -24,23 +24,22 @@
override def toString: String = string
}
- private val root = new DefaultMutableTreeNode
+ private val tree = new Tree_View(single_selection_mode = true)
+
for (section <- doc_contents.sections) {
- root.add(new DefaultMutableTreeNode(section.title))
+ tree.root.add(new DefaultMutableTreeNode(section.title))
section.entries.foreach(
{
case entry @ Doc.Doc(name, title, _) =>
val string = "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
- root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+ tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
.add(new DefaultMutableTreeNode(Node(string, entry)))
case entry @ Doc.Text_File(name: String, _) =>
- root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+ tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
.add(new DefaultMutableTreeNode(Node(name, entry)))
})
}
- private val tree = new Tree_View(root, single_selection_mode = true)
-
override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
private def action(node: DefaultMutableTreeNode): Unit = {
--- a/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 20:00:54 2024 +0100
+++ b/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 20:01:26 2024 +0100
@@ -13,7 +13,7 @@
import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
MouseEvent, MouseAdapter}
import javax.swing.JComponent
-import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel}
+import javax.swing.tree.DefaultMutableTreeNode
import javax.swing.event.TreeSelectionEvent
import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
@@ -28,28 +28,10 @@
/* tree view */
- val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name)
- 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 {
- case node: DefaultMutableTreeNode =>
- val obj = node.getUserObject
- if (obj != null && which.isDefinedAt(obj)) Some(which(obj))
- else None
- case _ => None
- }
+ val tree: Tree_View =
+ new Tree_View(root = new DefaultMutableTreeNode(root_name), single_selection_mode = true)
def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
-
- def clear(): Unit = {
- tree.clearSelection()
- root.removeAllChildren()
- }
-
- def reload(): Unit =
- tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
-
tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))