equal
deleted
inserted
replaced
12 |
12 |
13 import javax.swing.JPopupMenu |
13 import javax.swing.JPopupMenu |
14 import scala.swing.{Action, Menu, MenuItem, Separator} |
14 import scala.swing.{Action, Menu, MenuItem, Separator} |
15 |
15 |
16 |
16 |
17 object Popups |
17 object Popups { |
18 { |
|
19 def apply( |
18 def apply( |
20 graph_panel: Graph_Panel, |
19 graph_panel: Graph_Panel, |
21 mouse_node: Option[Graph_Display.Node], |
20 mouse_node: Option[Graph_Display.Node], |
22 selected_nodes: List[Graph_Display.Node]): JPopupMenu = |
21 selected_nodes: List[Graph_Display.Node] |
23 { |
22 ): JPopupMenu = { |
24 val graphview = graph_panel.graphview |
23 val graphview = graph_panel.graphview |
25 |
24 |
26 val add_mutator = graphview.model.Mutators.add _ |
25 val add_mutator = graphview.model.Mutators.add _ |
27 val visible_graph = graphview.visible_graph |
26 val visible_graph = graphview.visible_graph |
28 |
27 |