--- 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
}
--- 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()
--- 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("<stopped>")); true }
+ if (stopped) { data.root.add(Tree_View.Node("<stopped>")); true }
else ok
}
else false
- if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
+ if (!ok) data.root.add(Tree_View.Node("<ignored>"))
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)) + "</html>"
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
}
--- 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)
}
--- 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><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
- 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 _ =>
}
}
--- 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))