| changeset 67012 | 671decd2e627 |
| parent 66830 | 3b50269b90c2 |
| child 67018 | f6aa133f9b16 |
--- a/src/Pure/General/graph.scala Sun Nov 05 15:50:26 2017 +0100 +++ b/src/Pure/General/graph.scala Sun Nov 05 16:57:03 2017 +0100 @@ -70,6 +70,7 @@ def keys_iterator: Iterator[Key] = iterator.map(_._1) def keys: List[Key] = keys_iterator.toList + def keys_set: Set[Key] = rep.keySet def dest: List[((Key, A), List[Key])] = (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList