src/Pure/General/graph.ML
changeset 48350 09bf3b73e446
parent 46668 9034b44844bd
child 49560 11430dd89e35
equal deleted inserted replaced
48349:a78e5d399599 48350:09bf3b73e446
   142 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   142 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   143 fun reachable next xs =
   143 fun reachable next xs =
   144   let
   144   let
   145     fun reach x (rs, R) =
   145     fun reach x (rs, R) =
   146       if Keys.member R x then (rs, R)
   146       if Keys.member R x then (rs, R)
   147       else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
   147       else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
   148     fun reachs x (rss, R) =
   148     fun reachs x (rss, R) =
   149       reach x ([], R) |>> (fn rs => rs :: rss);
   149       reach x ([], R) |>> (fn rs => rs :: rss);
   150   in fold reachs xs ([], Keys.empty) end;
   150   in fold reachs xs ([], Keys.empty) end;
   151 
   151 
   152 (*immediate*)
   152 (*immediate*)