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() }