# HG changeset patch # User wenzelm # Date 1730663592 -3600 # Node ID 1775fdc7274e6711ac8d273ca54770d3cce9ce0f # Parent 46d1d072fda399057683bda708c840e422dfcd18 clarified signature; diff -r 46d1d072fda3 -r 1775fdc7274e src/Pure/GUI/tree_view.scala --- a/src/Pure/GUI/tree_view.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Pure/GUI/tree_view.scala Sun Nov 03 20:53:12 2024 +0100 @@ -7,19 +7,32 @@ package isabelle import javax.swing.JTree -import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} +import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel, + TreeSelectionModel} +object Tree_View { + type Node = DefaultMutableTreeNode + + object Node { + def apply(obj: AnyRef = null): Node = + if (obj == null) new DefaultMutableTreeNode else new DefaultMutableTreeNode(obj) + + def unapply(tree_node: MutableTreeNode): Option[AnyRef] = + tree_node match { + case node: Node => Some(node.getUserObject) + case _ => None + } + } +} + class Tree_View( - val root: DefaultMutableTreeNode = new DefaultMutableTreeNode, + val root: Tree_View.Node = Tree_View.Node(), 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 Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj)) case _ => None } diff -r 46d1d072fda3 -r 1775fdc7274e src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Tools/Graphview/tree_panel.scala Sun Nov 03 20:53:12 2024 +0100 @@ -11,7 +11,7 @@ import java.awt.{Dimension, Rectangle} import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter} -import javax.swing.tree.{DefaultMutableTreeNode, TreePath} +import javax.swing.tree.TreePath import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent} import scala.util.matching.Regex @@ -30,11 +30,7 @@ if (paths != null) { for (path <- paths if path != null) { path.getLastPathComponent match { - case tree_node: DefaultMutableTreeNode => - tree_node.getUserObject match { - case node: Graph_Display.Node => graphview.Selection.add(node) - case _ => - } + case Tree_View.Node(node: Graph_Display.Node) => graphview.Selection.add(node) case _ => } } @@ -47,11 +43,7 @@ if (tree_pane != null && path != null) { val action_node = path.getLastPathComponent match { - case tree_node: DefaultMutableTreeNode => - tree_node.getUserObject match { - case node: Graph_Display.Node => Some(node) - case _ => None - } + case Tree_View.Node(node: Graph_Display.Node) => Some(node) case _ => None } action_node.foreach(graph_panel.scroll_to_node(_)) @@ -65,7 +57,7 @@ private var nodes = List.empty[Graph_Display.Node] - val tree: Tree_View = new Tree_View(root = new DefaultMutableTreeNode("Nodes")) + val tree: Tree_View = new Tree_View(root = Tree_View.Node("Nodes")) tree.addKeyListener(new KeyAdapter { override def keyPressed(e: KeyEvent): Unit = @@ -151,7 +143,7 @@ tree.clear() nodes = new_nodes - for (node <- nodes) tree.root.add(new DefaultMutableTreeNode(node)) + for (node <- nodes) tree.root.add(Tree_View.Node(node)) tree.expandRow(0) tree.revalidate() diff -r 46d1d072fda3 -r 1775fdc7274e src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sun Nov 03 20:53:12 2024 +0100 @@ -11,7 +11,6 @@ import isabelle._ import isabelle.jedit._ -import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position import javax.swing.Icon @@ -65,8 +64,8 @@ def swing_markup_tree( tree: Markup_Tree, - parent: DefaultMutableTreeNode, - swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode + parent: Tree_View.Node, + swing_node: Text.Info[List[XML.Elem]] => Tree_View.Node ): Unit = { for ((_, entry) <- tree.branches) { val node = swing_node(Text.Info(entry.range, entry.markup)) @@ -97,11 +96,11 @@ val ok = if (syntax.isDefined) { val ok = parser(buffer, syntax.get, data) - if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true } + if (stopped) { data.root.add(Tree_View.Node("")); true } else ok } else false - if (!ok) data.root.add(new DefaultMutableTreeNode("")) + if (!ok) data.root.add(Tree_View.Node("")) data } @@ -115,7 +114,7 @@ ) extends Isabelle_Sidekick(name) { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { def make_tree( - parent: DefaultMutableTreeNode, + parent: Tree_View.Node, offset: Text.Offset, documents: List[Document_Structure.Document] ): Unit = { @@ -125,7 +124,7 @@ case Document_Structure.Block(name, text, body) => val range = Text.Range(i, i + document.length) val node = - new DefaultMutableTreeNode( + Tree_View.Node( new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) parent.add(node) make_tree(node, i, body) @@ -193,7 +192,7 @@ val content = command.source(info.range).replace('\n', ' ') val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString - new DefaultMutableTreeNode( + Tree_View.Node( new Isabelle_Sidekick.Asset(command.toString, range) { override def getShortString: String = content override def getLongString: String = info_text @@ -212,14 +211,14 @@ private val Heading1 = """^New in (.*)\w*$""".r private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r - private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = - new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) + private def make_node(s: String, start: Text.Offset, stop: Text.Offset): Tree_View.Node = + Tree_View.Node(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { var offset = 0 var end_offset = 0 - var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None + var start1: Option[(Int, String, Vector[Tree_View.Node])] = None var start2: Option[(Int, String)] = None def close1(): Unit = @@ -285,7 +284,7 @@ if_proper(name, " " + HTML.output(name)) + "" val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) - data.root.add(new DefaultMutableTreeNode(asset)) + data.root.add(Tree_View.Node(asset)) } offset += source.length } diff -r 46d1d072fda3 -r 1775fdc7274e src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Nov 03 20:53:12 2024 +0100 @@ -12,7 +12,6 @@ import java.awt.BorderLayout import java.awt.event.KeyEvent import javax.swing.JMenuItem -import javax.swing.tree.DefaultMutableTreeNode import javax.swing.event.TreeSelectionEvent import scala.collection.immutable.SortedMap @@ -123,9 +122,9 @@ output.tree.clear() for (thread <- thread_contexts) { - val thread_node = new DefaultMutableTreeNode(thread) + val thread_node = Tree_View.Node(thread) for ((_, i) <- thread.debug_states.zipWithIndex) - thread_node.add(new DefaultMutableTreeNode(thread.select(i))) + thread_node.add(Tree_View.Node(thread.select(i))) output.tree.root.add(thread_node) } diff -r 46d1d072fda3 -r 1775fdc7274e src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Sun Nov 03 20:53:12 2024 +0100 @@ -12,7 +12,6 @@ import java.awt.Dimension import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter} import javax.swing.JScrollPane -import javax.swing.tree.DefaultMutableTreeNode import org.gjt.sp.jedit.{View, OperatingSystem} @@ -27,22 +26,22 @@ private val tree = new Tree_View(single_selection_mode = true) for (section <- doc_contents.sections) { - tree.root.add(new DefaultMutableTreeNode(section.title)) + tree.root.add(Tree_View.Node(section.title)) section.entries.foreach( { case entry @ Doc.Doc(name, title, _) => val string = "" + HTML.output(name) + ": " + HTML.output(title) + "" - tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] - .add(new DefaultMutableTreeNode(Node(string, entry))) + tree.root.getLastChild.asInstanceOf[Tree_View.Node] + .add(Tree_View.Node(Node(string, entry))) case entry @ Doc.Text_File(name: String, _) => - tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] - .add(new DefaultMutableTreeNode(Node(name, entry))) + tree.root.getLastChild.asInstanceOf[Tree_View.Node] + .add(Tree_View.Node(Node(name, entry))) }) } override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow - private def action(node: DefaultMutableTreeNode): Unit = { + private def action(node: Tree_View.Node): Unit = { node.getUserObject match { case Node(_, Doc.Doc(_, _, path)) => PIDE.editor.goto_doc(view, path) @@ -59,7 +58,7 @@ val path = tree.getSelectionPath if (path != null) { path.getLastPathComponent match { - case node: DefaultMutableTreeNode => action(node) + case node: Tree_View.Node => action(node) case _ => } } @@ -71,8 +70,7 @@ val click = tree.getPathForLocation(e.getX, e.getY) if (click != null && e.getClickCount == 1) { (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { - case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => - action(node) + case (node: Tree_View.Node, node1: Tree_View.Node) if node == node1 => action(node) case _ => } } diff -r 46d1d072fda3 -r 1775fdc7274e src/Tools/jEdit/src/tree_text_area.scala --- a/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 20:23:19 2024 +0100 +++ b/src/Tools/jEdit/src/tree_text_area.scala Sun Nov 03 20:53:12 2024 +0100 @@ -13,7 +13,6 @@ import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent, MouseEvent, MouseAdapter} import javax.swing.JComponent -import javax.swing.tree.DefaultMutableTreeNode import javax.swing.event.TreeSelectionEvent import scala.swing.{Component, ScrollPane, SplitPane, Orientation} @@ -29,7 +28,7 @@ /* tree view */ val tree: Tree_View = - new Tree_View(root = new DefaultMutableTreeNode(root_name), single_selection_mode = true) + new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true) def handle_tree_selection(e: TreeSelectionEvent): Unit = () tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))