equal
deleted
inserted
replaced
45 extends Graph_Filter(name, description, g => g.restrict(pred(g, _))) |
45 extends Graph_Filter(name, description, g => g.restrict(pred(g, _))) |
46 |
46 |
47 class Edge_Filter( |
47 class Edge_Filter( |
48 name: String, |
48 name: String, |
49 description: String, |
49 description: String, |
50 pred: (Graph_Display.Graph, Graph_Display.Node, Graph_Display.Node) => Boolean) |
50 pred: (Graph_Display.Graph, Graph_Display.Edge) => Boolean) |
51 extends Graph_Filter( |
51 extends Graph_Filter( |
52 name, |
52 name, |
53 description, |
53 description, |
54 g => (g /: g.dest) { |
54 g => (g /: g.dest) { |
55 case (graph, ((from, _), tos)) => |
55 case (graph, ((from, _), tos)) => |
56 (graph /: tos)((gr, to) => |
56 (graph /: tos)((gr, to) => |
57 if (pred(gr, from, to)) gr else gr.del_edge(from, to)) |
57 if (pred(gr, (from, to))) gr else gr.del_edge(from, to)) |
58 }) |
58 }) |
59 |
59 |
60 class Node_Family_Filter( |
60 class Node_Family_Filter( |
61 name: String, |
61 name: String, |
62 description: String, |
62 description: String, |
103 reverse, |
103 reverse, |
104 parents, |
104 parents, |
105 children, |
105 children, |
106 (g, node) => list.contains(node)) |
106 (g, node) => list.contains(node)) |
107 |
107 |
108 case class Edge_Endpoints(source: Graph_Display.Node, dest: Graph_Display.Node) |
108 case class Edge_Endpoints(edge: Graph_Display.Edge) |
109 extends Edge_Filter( |
109 extends Edge_Filter( |
110 "Hide edge", |
110 "Hide edge", |
111 "Hides the edge whose endpoints match strings.", |
111 "Hides specified edge.", |
112 (g, s, d) => !(s == source && d == dest)) |
112 (g, e) => e != edge) |
113 |
113 |
114 private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph, |
114 private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph, |
115 keys: List[Graph_Display.Node]) = |
115 keys: List[Graph_Display.Node]) = |
116 { |
116 { |
117 // Add Nodes |
117 // Add Nodes |