equal
deleted
inserted
replaced
140 popup.add(filter_context(selected_nodes, true, "Hide", true).peer) |
140 popup.add(filter_context(selected_nodes, true, "Hide", true).peer) |
141 popup.add(filter_context(selected_nodes, false, "Show only", false).peer) |
141 popup.add(filter_context(selected_nodes, false, "Show only", false).peer) |
142 popup.add(new JPopupMenu.Separator) |
142 popup.add(new JPopupMenu.Separator) |
143 } |
143 } |
144 |
144 |
145 popup.add( |
145 popup.add(new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer) |
146 new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer) |
|
147 |
146 |
148 popup |
147 popup |
149 } |
148 } |
150 } |
149 } |