--- a/src/Pure/General/multi_map.scala Mon Dec 01 14:24:05 2014 +0100
+++ b/src/Pure/General/multi_map.scala Mon Dec 01 15:21:49 2014 +0100
@@ -21,7 +21,7 @@
}
-final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
+final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
extends scala.collection.immutable.Map[A, B]
with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
{
@@ -50,6 +50,14 @@
else this
}
+ def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] =
+ if (this eq other) this
+ else if (isEmpty) other
+ else
+ (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
+ case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
+ }
+
/* Map operations */