author | wenzelm |
Sun, 03 Nov 2024 20:05:06 +0100 | |
changeset 81326 | 403203217493 |
parent 81325 | 458e9e3b356e |
child 81327 | 2529568daaff |
--- a/src/Pure/GUI/tree_view.scala Sun Nov 03 20:01:26 2024 +0100 +++ b/src/Pure/GUI/tree_view.scala Sun Nov 03 20:05:06 2024 +0100 @@ -29,7 +29,10 @@ } def reload_model(): Unit = - getModel.asInstanceOf[DefaultTreeModel].reload(root) + getModel match { + case model: DefaultTreeModel => model.reload(root) + case _ => + } /* init */