removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;

--- a/src/Tools/Graphview/src/model.scala	Mon Dec 10 16:38:20 2012 +0100
+++ b/src/Tools/Graphview/src/model.scala	Mon Dec 10 17:05:51 2012 +0100
@@ -64,7 +64,6 @@
       Node_Expression(".*", false, false, false),
       Node_List(Nil, false, false, false),
       Edge_Endpoints("", ""),
-      Edge_Transitive(),
       Add_Node_Expression(""),
       Add_Transitive_Closure(true, true)
     ))

--- a/src/Tools/Graphview/src/mutator.scala	Mon Dec 10 16:38:20 2012 +0100
+++ b/src/Tools/Graphview/src/mutator.scala	Mon Dec 10 17:05:51 2012 +0100
@@ -133,17 +133,6 @@
     (g, s, d) => !(s == source && d == dest)
   )
 
-  case class Edge_Transitive()  // FIXME slow! / obsolete?!
-    extends Edge_Filter(
-
-    "Hide transitive edges",
-    "Hides all transitive edges.",
-    (g, s, d) => {
-      !g.imm_succs(s).filter(_ != d)  // FIXME iterator
-      .exists(p => !(g.irreducible_paths(p, d).isEmpty))
-    }
-  )
-
   private def add_node_group(from: Model.Graph, to: Model.Graph,
     keys: List[String]) = {
     

--- a/src/Tools/Graphview/src/mutator_dialog.scala	Mon Dec 10 16:38:20 2012 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala	Mon Dec 10 17:05:51 2012 +0100
@@ -286,8 +286,6 @@
             inputs(0)._2.getString,
             inputs(1)._2.getString
           )
-        case Edge_Transitive() =>
-          Edge_Transitive()
         case Add_Node_Expression(r) =>
           Add_Node_Expression(
             regexOrElse(inputs(0)._2.getString, r)

--- a/src/Tools/Graphview/src/popups.scala	Mon Dec 10 16:38:20 2012 +0100
+++ b/src/Tools/Graphview/src/popups.scala	Mon Dec 10 17:05:51 2012 +0100
@@ -130,10 +130,6 @@
           def apply = panel.visualizer.model.Mutators(Nil)
         }).peer
     )
-    popup.add(new MenuItem(new Action("Remove transitive edges") {
-          def apply = add_mutator(Mutators.create(Edge_Transitive()))
-        }).peer
-    )
     popup.add(new JPopupMenu.Separator)
 
     if (under_mouse.isDefined) {