# HG changeset patch # User wenzelm # Date 1355155551 -3600 # Node ID 1d7e506a3a77b13e52acdc579852f17560345224 # Parent 3453285475d1d48731c45515088443804e9f395d removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently; diff -r 3453285475d1 -r 1d7e506a3a77 src/Tools/Graphview/src/model.scala --- 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) )) diff -r 3453285475d1 -r 1d7e506a3a77 src/Tools/Graphview/src/mutator.scala --- 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]) = { diff -r 3453285475d1 -r 1d7e506a3a77 src/Tools/Graphview/src/mutator_dialog.scala --- 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) diff -r 3453285475d1 -r 1d7e506a3a77 src/Tools/Graphview/src/popups.scala --- 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) {