src/Pure/General/multi_map.scala
changeset 59073 dcecfcc56dce
parent 56744 0b74d1df4b8e
child 63579 73939a9b70a3
     1.1 --- a/src/Pure/General/multi_map.scala	Mon Dec 01 14:24:05 2014 +0100
     1.2 +++ b/src/Pure/General/multi_map.scala	Mon Dec 01 15:21:49 2014 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  }
     1.5  
     1.6  
     1.7 -final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
     1.8 +final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
     1.9    extends scala.collection.immutable.Map[A, B]
    1.10    with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
    1.11  {
    1.12 @@ -50,6 +50,14 @@
    1.13      else this
    1.14    }
    1.15  
    1.16 +  def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] =
    1.17 +    if (this eq other) this
    1.18 +    else if (isEmpty) other
    1.19 +    else
    1.20 +      (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
    1.21 +        case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
    1.22 +      }
    1.23 +
    1.24  
    1.25    /* Map operations */
    1.26