tuned;

--- a/src/Tools/Graphview/tree_panel.scala	Sun Nov 03 20:15:12 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sun Nov 03 20:23:19 2024 +0100
@@ -148,11 +148,9 @@
   def refresh(): Unit = {
     val new_nodes = graphview.visible_graph.topological_order
     if (new_nodes != nodes) {
-      tree.clearSelection
+      tree.clear()
 
       nodes = new_nodes
-
-      tree.root.removeAllChildren
       for (node <- nodes) tree.root.add(new DefaultMutableTreeNode(node))
 
       tree.expandRow(0)