# HG changeset patch
# User wenzelm
# Date 1342705559 -7200
# Node ID 09bf3b73e446c37b4a107c6a7ab31ae67c7bf42d
# Parent  a78e5d3995993cca9dbff9cba1b2d2ef950aebb7
clarified topological ordering: preserve order of adjacency via reverse fold;

diff -r a78e5d399599 -r 09bf3b73e446 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Thu Jul 19 14:24:40 2012 +0200
+++ b/src/Pure/General/graph.ML	Thu Jul 19 15:45:59 2012 +0200
@@ -144,7 +144,7 @@
   let
     fun reach x (rs, R) =
       if Keys.member R x then (rs, R)
-      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
+      else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
     fun reachs x (rss, R) =
       reach x ([], R) |>> (fn rs => rs :: rss);
   in fold reachs xs ([], Keys.empty) end;
diff -r a78e5d399599 -r 09bf3b73e446 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Jul 19 14:24:40 2012 +0200
+++ b/src/Pure/General/graph.scala	Thu Jul 19 15:45:59 2012 +0200
@@ -73,19 +73,19 @@
   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
   {
-    def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
+    def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
     {
       val (rs, r_set) = reached
       if (r_set(x)) reached
       else {
-        val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
+        val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
         (x :: rs1, r_set1)
       }
     }
     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
     {
       val (rss, r_set) = reached
-      val (rs, r_set1) = reach((Nil, r_set), x)
+      val (rs, r_set1) = reach(x, (Nil, r_set))
       (rs :: rss, r_set1)
     }
     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
diff -r a78e5d399599 -r 09bf3b73e446 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 19 14:24:40 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 19 15:45:59 2012 +0200
@@ -26,7 +26,7 @@
       object Ordering extends scala.math.Ordering[Key]
       {
         def compare(key1: Key, key2: Key): Int =
-          key2.order compare key1.order match {
+          key1.order compare key2.order match {
             case 0 => key1.name compare key2.name
             case ord => ord
           }