equal
deleted
inserted
replaced
68 |
68 |
69 def iterator: Iterator[(Key, Entry)] = rep.iterator |
69 def iterator: Iterator[(Key, Entry)] = rep.iterator |
70 |
70 |
71 def keys_iterator: Iterator[Key] = iterator.map(_._1) |
71 def keys_iterator: Iterator[Key] = iterator.map(_._1) |
72 def keys: List[Key] = keys_iterator.toList |
72 def keys: List[Key] = keys_iterator.toList |
73 def keys_set: Set[Key] = rep.keySet |
|
74 |
73 |
75 def dest: List[((Key, A), List[Key])] = |
74 def dest: List[((Key, A), List[Key])] = |
76 (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList |
75 (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList |
77 |
76 |
78 override def toString: String = |
77 override def toString: String = |