src/Pure/GUI/tree_view.scala
changeset 81483 7d4df25af572
parent 81380 83012fe97282
child 81494 b30dc7db521f
--- 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 =