equal
deleted
inserted
replaced
6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 |
10 |
|
11 import scala.collection.GenTraversableOnce |
11 import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom} |
12 import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom} |
12 |
13 |
13 |
14 |
14 object Multi_Map extends ImmutableMapFactory[Multi_Map] |
15 object Multi_Map extends ImmutableMapFactory[Multi_Map] |
15 { |
16 { |
73 |
74 |
74 def get(a: A): Option[B] = get_list(a).headOption |
75 def get(a: A): Option[B] = get_list(a).headOption |
75 |
76 |
76 def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2) |
77 def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2) |
77 |
78 |
|
79 override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] = |
|
80 (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _) |
|
81 |
78 def - (a: A): Multi_Map[A, B] = |
82 def - (a: A): Multi_Map[A, B] = |
79 if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this |
83 if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this |
80 } |
84 } |