# HG changeset patch
# User wenzelm
# Date 1376307054 -7200
# Node ID 457c006f91bb440fdfb289e6f55be5e83840395e
# Parent  908e8a36e97567b8e128da74242bd971acb2b36f
support for maps with multiple entries per key;

diff -r 908e8a36e975 -r 457c006f91bb src/Pure/General/multi_map.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/multi_map.scala	Mon Aug 12 13:30:54 2013 +0200
@@ -0,0 +1,68 @@
+/*  Title:      Pure/General/multi_map.scala
+    Module:     PIDE
+
+Maps with multiple entries per key.
+*/
+
+package isabelle
+
+import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
+
+
+object Multi_Map extends ImmutableMapFactory[Multi_Map]
+{
+  private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
+  override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+
+  implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
+    new MapCanBuildFrom[A, B]
+}
+
+
+final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
+  extends scala.collection.immutable.Map[A, B]
+  with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
+{
+  /* Multi_Map operations */
+
+  def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
+
+  def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
+  {
+    val bs = get_list(a)
+    if (bs.contains(b)) this
+    else new Multi_Map(rep + (a -> (b :: bs)))
+  }
+
+  def remove[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
+  {
+    val bs = get_list(a)
+    if (bs.contains(b)) {
+      bs.filterNot(_ == b) match {
+        case Nil => new Multi_Map(rep - a)
+        case bs1 => new Multi_Map(rep + (a -> bs1))
+      }
+    }
+    else this
+  }
+
+
+  /* Map operations */
+
+  override def stringPrefix = "Multi_Map"
+
+  override def empty = Multi_Map.empty
+  override def isEmpty: Boolean = rep.isEmpty
+
+  override def keySet: Set[A] = rep.keySet
+
+  override def iterator: Iterator[(A, B)] =
+    for ((a, bs) <- rep.iterator; b <- bs.iterator) yield (a, b)
+
+  def get(a: A): Option[B] = get_list(a).headOption
+
+  def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
+
+  def - (a: A): Multi_Map[A, B] =
+    if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
+}
diff -r 908e8a36e975 -r 457c006f91bb src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 12 12:06:48 2013 +0200
+++ b/src/Pure/build-jars	Mon Aug 12 13:30:54 2013 +0200
@@ -18,6 +18,7 @@
   General/graph.scala
   General/graphics_file.scala
   General/linear_set.scala
+  General/multi_map.scala
   General/path.scala
   General/position.scala
   General/pretty.scala