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