src/Tools/Graphview/tree_panel.scala
changeset 60846 a7e3f11c19b7
parent 60292 ba3c716144dd
child 60849 6e49311ef842
--- a/src/Tools/Graphview/tree_panel.scala	Wed Aug 05 16:22:56 2015 +0200
+++ b/src/Tools/Graphview/tree_panel.scala	Wed Aug 05 20:02:44 2015 +0200
@@ -152,12 +152,13 @@
   {
     val new_nodes = graphview.visible_graph.topological_order
     if (new_nodes != nodes) {
+      tree.clearSelection
+
       nodes = new_nodes
 
       root.removeAllChildren
       for (node <- nodes) root.add(new DefaultMutableTreeNode(node))
 
-      tree.clearSelection
       for (i <- 0 until tree.getRowCount) tree.expandRow(i)
       tree.revalidate()
     }