src/Pure/General/graph.scala
equal inserted replaced
48349:a78e5d399599 48350:09bf3b73e446
`    71   /* reachability */`
`    71   /* reachability */`
`    72 `
`    72 `
`    73   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/`
`    73   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/`
`    74   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =`
`    74   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =`
`    75   {`
`    75   {`
`    76     def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =`
`    76     def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =`
`    77     {`
`    77     {`
`    78       val (rs, r_set) = reached`
`    78       val (rs, r_set) = reached`
`    79       if (r_set(x)) reached`
`    79       if (r_set(x)) reached`
`    80       else {`
`    80       else {`
`    81         val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)`
`    81         val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)`
`    82         (x :: rs1, r_set1)`
`    82         (x :: rs1, r_set1)`
`    83       }`
`    83       }`
`    84     }`
`    84     }`
`    85     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =`
`    85     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =`
`    86     {`
`    86     {`
`    87       val (rss, r_set) = reached`
`    87       val (rss, r_set) = reached`
`    88       val (rs, r_set1) = reach((Nil, r_set), x)`
`    88       val (rs, r_set1) = reach(x, (Nil, r_set))`
`    89       (rs :: rss, r_set1)`
`    89       (rs :: rss, r_set1)`
`    90     }`
`    90     }`
`    91     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)`
`    91     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)`
`    92   }`
`    92   }`
`    93 `
`    93 `