# HG changeset patch
# User wenzelm
# Date 1355483768 -3600
# Node ID 5b7150395568f8f08247265d72a7b0c4de08f622
# Parent  9605b0d93d1e5a1b71dd379f6adc228b50cbeb11
tuned implementation according to Library.insert/merge in ML;

diff -r 9605b0d93d1e -r 5b7150395568 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Dec 14 12:09:08 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Dec 14 12:16:08 2012 +0100
@@ -25,13 +25,20 @@
     def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
   }
 
-  final class Results private(private val rep: SortedMap[Long, XML.Tree])
+  final class Results private(rep: SortedMap[Long, XML.Tree])
   {
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Tree] = rep.get(serial)
     def entries: Iterator[(Long, XML.Tree)] = rep.iterator
-    def + (entry: (Long, XML.Tree)): Results = new Results(rep + entry)
-    def ++ (other: Results): Results = new Results(rep ++ other.rep)
+
+    def + (entry: (Long, XML.Tree)): Results =
+      if (defined(entry._1)) this
+      else new Results(rep + entry)
+
+    def ++ (other: Results): Results =
+      if (this eq other) this
+      else if (rep.isEmpty) other
+      else (this /: other.entries)(_ + _)
   }