--- a/src/Pure/GUI/tree_view.scala Mon Nov 18 14:47:17 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala Mon Nov 18 15:05:31 2024 +0100
@@ -36,9 +36,12 @@
case _ => None
}
- def clear(): Unit = {
+ def init_model(body: => Unit): Unit = {
clearSelection()
root.removeAllChildren()
+ body
+ expandRow(0)
+ reload_model()
}
def reload_model(): Unit =
--- a/src/Tools/Graphview/tree_panel.scala Mon Nov 18 14:47:17 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Mon Nov 18 15:05:31 2024 +0100
@@ -140,14 +140,9 @@
def refresh(): Unit = {
val new_nodes = graphview.visible_graph.topological_order
- if (new_nodes != nodes) {
- tree.clear()
-
+ if (nodes != new_nodes) {
nodes = new_nodes
- for (node <- nodes) tree.root.add(Tree_View.Node(node))
-
- tree.expandRow(0)
- tree.revalidate()
+ tree.init_model { for (node <- nodes) tree.root.add(Tree_View.Node(node)) }
}
revalidate()
repaint()
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Nov 18 14:47:17 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Nov 18 15:05:31 2024 +0100
@@ -112,18 +112,16 @@
case _ => thread_contexts.headOption
}
- output.tree.clear()
-
- for (thread <- thread_contexts) {
- val thread_node = Tree_View.Node(thread)
- for ((_, i) <- thread.debug_states.zipWithIndex)
- thread_node.add(Tree_View.Node(thread.select(i)))
- output.tree.root.add(thread_node)
+ output.tree.init_model {
+ for (thread <- thread_contexts) {
+ val thread_node = Tree_View.Node(thread)
+ for ((_, i) <- thread.debug_states.zipWithIndex) {
+ thread_node.add(Tree_View.Node(thread.select(i)))
+ }
+ output.tree.root.add(thread_node)
+ }
}
- output.tree.reload_model()
-
- output.tree.expandRow(0)
for (i <- Range.inclusive(output.tree.getRowCount - 1, 1, -1)) output.tree.expandRow(i)
new_tree_selection match {
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Nov 18 14:47:17 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Nov 18 15:05:31 2024 +0100
@@ -31,10 +31,7 @@
private val output: Output_Area =
new Output_Area(view, root_name = "Search results") {
override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
- tree.clear()
- for (result <- search.results) tree.root.add(Tree_View.Node(result))
- tree.reload_model()
- tree.expandRow(0)
+ tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
tree.revalidate()
}
override def handle_update(): Unit = dockable.handle_update(true)