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 =