summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 19 Jul 2012 15:45:59 +0200 | |

changeset 48350 | 09bf3b73e446 |

parent 48349 | a78e5d399599 |

child 48351 | a0b95a762abb |

clarified topological ordering: preserve order of adjacency via reverse fold;

--- 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;

--- 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)

--- 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 }