# HG changeset patch # User wenzelm # Date 1420313333 -3600 # Node ID 32903b99c2ef36a8b843bd290f4cde41b371f40a # Parent be4180f3c236d076486491fb4cd3ae2be4f39c6f tuned signature; diff -r be4180f3c236 -r 32903b99c2ef src/Tools/Graphview/model.scala --- a/src/Tools/Graphview/model.scala Sat Jan 03 20:22:27 2015 +0100 +++ b/src/Tools/Graphview/model.scala Sat Jan 03 20:28:53 2015 +0100 @@ -40,7 +40,7 @@ List( Mutator.Node_Expression(".*", false, false, false), Mutator.Node_List(Nil, false, false, false), - Mutator.Edge_Endpoints(Graph_Display.Node.dummy, Graph_Display.Node.dummy), + Mutator.Edge_Endpoints((Graph_Display.Node.dummy, Graph_Display.Node.dummy)), Mutator.Add_Node_Expression(""), Mutator.Add_Transitive_Closure(true, true))) diff -r be4180f3c236 -r 32903b99c2ef src/Tools/Graphview/mutator.scala --- a/src/Tools/Graphview/mutator.scala Sat Jan 03 20:22:27 2015 +0100 +++ b/src/Tools/Graphview/mutator.scala Sat Jan 03 20:28:53 2015 +0100 @@ -47,14 +47,14 @@ class Edge_Filter( name: String, description: String, - pred: (Graph_Display.Graph, Graph_Display.Node, Graph_Display.Node) => Boolean) + pred: (Graph_Display.Graph, Graph_Display.Edge) => Boolean) extends Graph_Filter( name, description, g => (g /: g.dest) { case (graph, ((from, _), tos)) => (graph /: tos)((gr, to) => - if (pred(gr, from, to)) gr else gr.del_edge(from, to)) + if (pred(gr, (from, to))) gr else gr.del_edge(from, to)) }) class Node_Family_Filter( @@ -105,11 +105,11 @@ children, (g, node) => list.contains(node)) - case class Edge_Endpoints(source: Graph_Display.Node, dest: Graph_Display.Node) + case class Edge_Endpoints(edge: Graph_Display.Edge) extends Edge_Filter( "Hide edge", - "Hides the edge whose endpoints match strings.", - (g, s, d) => !(s == source && d == dest)) + "Hides specified edge.", + (g, e) => e != edge) private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph, keys: List[Graph_Display.Node]) = diff -r be4180f3c236 -r 32903b99c2ef src/Tools/Graphview/mutator_dialog.scala --- a/src/Tools/Graphview/mutator_dialog.scala Sat Jan 03 20:22:27 2015 +0100 +++ b/src/Tools/Graphview/mutator_dialog.scala Sat Jan 03 20:28:53 2015 +0100 @@ -269,10 +269,10 @@ // "Parents" means "Show parents" or "Matching Children" inputs(1)._2.bool, inputs(0)._2.bool) - case Mutator.Edge_Endpoints(_, _) => + case Mutator.Edge_Endpoints(_) => (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match { case (Some(node1), Some(node2)) => - Mutator.Edge_Endpoints(node1, node2) + Mutator.Edge_Endpoints((node1, node2)) case _ => Mutator.Identity() } @@ -304,7 +304,7 @@ ("", new Check_Box_Input("Children", check_parents)), ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))), ("", new Check_Box_Input(reverse_caption, reverse))) - case Mutator.Edge_Endpoints(source, dest) => + case Mutator.Edge_Endpoints((source, dest)) => List( ("Source", new Text_Field_Input(source.ident)), ("Destination", new Text_Field_Input(dest.ident))) diff -r be4180f3c236 -r 32903b99c2ef src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Sat Jan 03 20:22:27 2015 +0100 +++ b/src/Tools/Graphview/popups.scala Sat Jan 03 20:28:53 2015 +0100 @@ -81,7 +81,7 @@ new Action(to.toString) { def apply = add_mutator( - Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to))) + Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) }) }) } @@ -103,7 +103,7 @@ new Action(from.toString) { def apply = add_mutator( - Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to))) + Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) }) }) }