# HG changeset patch
# User wenzelm
# Date 1730660706 -3600
# Node ID 403203217493e6f6fe1a32690ab882f76a07df05
# Parent  458e9e3b356e902ee8b733a06fc5a8aa90ebb6fd
more robust;

diff -r 458e9e3b356e -r 403203217493 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 */