# HG changeset patch
# User wenzelm
# Date 1731938731 -3600
# Node ID 7d4df25af57271580033552c80edbec2eff2e44f
# Parent  1001e27dbbf16709bcd147dbc29eb1c270ee292d
clarified Tree_View.init_model: more uniform;

diff -r 1001e27dbbf1 -r 7d4df25af572 src/Pure/GUI/tree_view.scala
--- 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 =
diff -r 1001e27dbbf1 -r 7d4df25af572 src/Tools/Graphview/tree_panel.scala
--- 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()
diff -r 1001e27dbbf1 -r 7d4df25af572 src/Tools/jEdit/src/debugger_dockable.scala
--- 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 {
diff -r 1001e27dbbf1 -r 7d4df25af572 src/Tools/jEdit/src/output_dockable.scala
--- 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)