diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Jul 05 16:01:45 2013 +0200
@@ -75,7 +75,7 @@
     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.ID, message: XML.Elem): State =
+    def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>