# 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))))
                               })
                         })
                       }