equal
deleted
inserted
replaced
150 |
150 |
151 def refresh() |
151 def refresh() |
152 { |
152 { |
153 val new_nodes = graphview.visible_graph.topological_order |
153 val new_nodes = graphview.visible_graph.topological_order |
154 if (new_nodes != nodes) { |
154 if (new_nodes != nodes) { |
|
155 tree.clearSelection |
|
156 |
155 nodes = new_nodes |
157 nodes = new_nodes |
156 |
158 |
157 root.removeAllChildren |
159 root.removeAllChildren |
158 for (node <- nodes) root.add(new DefaultMutableTreeNode(node)) |
160 for (node <- nodes) root.add(new DefaultMutableTreeNode(node)) |
159 |
161 |
160 tree.clearSelection |
|
161 for (i <- 0 until tree.getRowCount) tree.expandRow(i) |
162 for (i <- 0 until tree.getRowCount) tree.expandRow(i) |
162 tree.revalidate() |
163 tree.revalidate() |
163 } |
164 } |
164 revalidate() |
165 revalidate() |
165 repaint() |
166 repaint() |