summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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