# HG changeset patch # User wenzelm # Date 1355147147 -3600 # Node ID 75e00ff42870551870c9727a663ebad19d9dacb7 # Parent 0a740d127187742f6192e0895f9c58f272574bf0# Parent 2e22cdccdc38b5e4e79bd9501ef293f634e0398c merged diff -r 0a740d127187 -r 75e00ff42870 src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Mon Dec 10 10:29:52 2012 +0100 +++ b/src/Pure/General/graph.scala Mon Dec 10 14:45:47 2012 +0100 @@ -224,17 +224,16 @@ /* transitive closure and reduction */ - def transitive_closure: Graph[Key, A] = + private def transitive_step(z: Key): Graph[Key, A] = { + val (preds, succs) = get_entry(z)._2 var graph = this - for { - (_, (_, (preds, succs))) <- this.entries - x <- preds - y <- succs - } graph = graph.add_edge(x, y) + for (x <- preds; y <- succs) graph = graph.add_edge(x, y) graph } + def transitive_closure: Graph[Key, A] = (this /: keys)(_.transitive_step(_)) + def transitive_reduction_acyclic: Graph[Key, A] = { val trans = this.transitive_closure