# HG changeset patch
# User wenzelm
# Date 1730661799 -3600
# Node ID 46d1d072fda399057683bda708c840e422dfcd18
# Parent  2529568daaff000a001560751e178e64ac00e5ad
tuned;

diff -r 2529568daaff -r 46d1d072fda3 src/Tools/Graphview/tree_panel.scala
--- 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)