--- 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) =>