src/Pure/General/multi_map.scala
changeset 55488 60c159d490a2
parent 52975 457c006f91bb
child 55618 995162143ef4
equal deleted inserted replaced
55476:e2cf2df4fd83 55488:60c159d490a2
    22 final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
    22 final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
    23   extends scala.collection.immutable.Map[A, B]
    23   extends scala.collection.immutable.Map[A, B]
    24   with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
    24   with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
    25 {
    25 {
    26   /* Multi_Map operations */
    26   /* Multi_Map operations */
       
    27 
       
    28   def iterator_list: Iterator[(A, List[B])] = rep.iterator
    27 
    29 
    28   def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
    30   def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
    29 
    31 
    30   def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
    32   def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
    31   {
    33   {