22 selected_nodes: List[Graph_Display.Node]): JPopupMenu = |
22 selected_nodes: List[Graph_Display.Node]): JPopupMenu = |
23 { |
23 { |
24 val visualizer = panel.visualizer |
24 val visualizer = panel.visualizer |
25 |
25 |
26 val add_mutator = visualizer.model.Mutators.add _ |
26 val add_mutator = visualizer.model.Mutators.add _ |
27 val curr = visualizer.model.current_graph |
27 val current_graph = visualizer.model.current_graph |
28 |
28 |
29 def filter_context( |
29 def filter_context( |
30 nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) = |
30 nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) = |
31 new Menu(caption) { |
31 new Menu(caption) { |
32 contents += |
32 contents += |
52 def apply = |
52 def apply = |
53 add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false))) |
53 add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false))) |
54 }) |
54 }) |
55 |
55 |
56 if (edges) { |
56 if (edges) { |
57 val outs = |
57 def degree_nodes(succs: Boolean) = |
58 nodes.map(l => (l, curr.imm_succs(l))) // FIXME iterator |
58 (for { |
59 .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering) |
59 from <- nodes.iterator |
60 val ins = |
60 tos = if (succs) current_graph.imm_succs(from) else current_graph.imm_preds(from) |
61 nodes.map(l => (l, curr.imm_preds(l))) // FIXME iterator |
61 if tos.nonEmpty |
62 .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering) |
62 } yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering) |
|
63 |
|
64 val outs = degree_nodes(true) |
|
65 val ins = degree_nodes(false) |
63 |
66 |
64 if (outs.nonEmpty || ins.nonEmpty) { |
67 if (outs.nonEmpty || ins.nonEmpty) { |
65 contents += new Separator() |
68 contents += new Separator() |
66 |
|
67 contents += |
69 contents += |
68 new Menu("Edge") { |
70 new Menu("Edge") { |
69 if (outs.nonEmpty) { |
71 if (outs.nonEmpty) { |
70 contents += new MenuItem("From ...") { enabled = false } |
72 contents += new MenuItem("From ...") { enabled = false } |
71 |
73 for ((from, tos) <- outs) { |
72 outs.map(e => { |
|
73 val (from, tos) = e |
|
74 contents += |
74 contents += |
75 new Menu(quote(from.toString)) { |
75 new Menu(quote(from.toString)) { |
76 contents += new MenuItem("To ...") { enabled = false } |
76 contents += new MenuItem("To ...") { enabled = false } |
77 |
77 for (to <- tos) { |
78 tos.toList.sorted(Graph_Display.Node.Ordering).distinct.map(to => { |
|
79 contents += |
78 contents += |
80 new MenuItem( |
79 new MenuItem( |
81 new Action(quote(to.toString)) { |
80 new Action(quote(to.toString)) { |
82 def apply = |
81 def apply = |
83 add_mutator( |
82 add_mutator( |
84 Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
83 Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
85 }) |
84 }) |
86 }) |
85 } |
87 } |
86 } |
88 }) |
87 } |
89 } |
88 } |
90 if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() } |
89 if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() } |
91 if (ins.nonEmpty) { |
90 if (ins.nonEmpty) { |
92 contents += new MenuItem("To ...") { enabled = false } |
91 contents += new MenuItem("To ...") { enabled = false } |
93 |
92 for ((to, froms) <- ins) { |
94 ins.map(e => { |
|
95 val (to, froms) = e |
|
96 contents += |
93 contents += |
97 new Menu(quote(to.toString)) { |
94 new Menu(quote(to.toString)) { |
98 contents += new MenuItem("From ...") { enabled = false } |
95 contents += new MenuItem("From ...") { enabled = false } |
99 |
96 for (from <- froms) { |
100 froms.toList.sorted(Graph_Display.Node.Ordering).distinct.map(from => { |
|
101 contents += |
97 contents += |
102 new MenuItem( |
98 new MenuItem( |
103 new Action(quote(from.toString)) { |
99 new Action(quote(from.toString)) { |
104 def apply = |
100 def apply = |
105 add_mutator( |
101 add_mutator( |
106 Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
102 Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
107 }) |
103 }) |
108 }) |
104 } |
109 } |
105 } |
110 }) |
106 } |
111 } |
107 } |
112 } |
108 } |
113 } |
109 } |
114 } |
110 } |
115 } |
111 } |