more robust;
authorwenzelm
Sun, 03 Nov 2024 20:05:06 +0100
changeset 81326 403203217493
parent 81325 458e9e3b356e
child 81327 2529568daaff
more robust;
src/Pure/GUI/tree_view.scala
--- 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 */