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 =