# HG changeset patch # User wenzelm # Date 1730660486 -3600 # Node ID 458e9e3b356e902ee8b733a06fc5a8aa90ebb6fd # Parent 0ec5131899b679a8aa721e399dc76bda91a406f4 clarified signature; diff -r 0ec5131899b6 -r 458e9e3b356e 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") } } diff -r 0ec5131899b6 -r 458e9e3b356e src/Tools/Graphview/tree_panel.scala --- 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() diff -r 0ec5131899b6 -r 458e9e3b356e src/Tools/jEdit/src/debugger_dockable.scala --- 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) diff -r 0ec5131899b6 -r 458e9e3b356e src/Tools/jEdit/src/documentation_dockable.scala --- 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.output(name) + ": " + HTML.output(title) + "" - 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 = { diff -r 0ec5131899b6 -r 458e9e3b356e src/Tools/jEdit/src/tree_text_area.scala --- 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))