src/Pure/PIDE/command.scala
changeset 52531 21f8e0e151f5
parent 52530 99dd8b4ef3fe
child 52535 b7badd371e4d
--- 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) =>