# HG changeset patch
# User wenzelm
# Date 1355132489 -3600
# Node ID 2e22cdccdc38b5e4e79bd9501ef293f634e0398c
# Parent  8dc05db0bf69ed9d347447226698813f6822ead7
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;

diff -r 8dc05db0bf69 -r 2e22cdccdc38 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sun Dec 09 14:05:21 2012 +0100
+++ b/src/Pure/General/graph.scala	Mon Dec 10 10:41:29 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