src/Pure/PIDE/command.scala

   {
     val empty = new Results(SortedMap.empty)
     def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
   }
 
-  final class Results private(rep: SortedMap[Long, XML.Tree])
+  final class Results private(private val 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 ++ (other: Results): Results =
       if (this eq other) this
       else if (rep.isEmpty) other
       else (this /: other.entries)(_ + _)
 
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Results => rep == other.rep
+        case _ => false
+      }
     override def toString: String = entries.mkString("Results(", ", ", ")")
   }
 
 
   /* state */

   {
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
       markup.to_XML(command.range, command.source, filter)
 
 
-    /* accumulate content */
+    /* content */
+
+    def eq_content(other: State): Boolean =
+      command.source == other.command.source &&
+      status == other.status &&
+      results == other.results &&
+      markup == other.markup
 
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
 
     def + (alt_id: Document.ID, message: XML.Elem): Command.State =