diff -r c13c95c97e89 -r 9951852fae91 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Aug 15 23:13:56 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 16 00:07:28 2010 +0200
@@ -14,14 +14,6 @@
 
 object Command
 {
-  object Status extends Enumeration
-  {
-    val UNPROCESSED = Value("UNPROCESSED")
-    val FINISHED = Value("FINISHED")
-    val FAILED = Value("FAILED")
-    val UNDEFINED = Value("UNDEFINED")
-  }
-
   case class HighlightInfo(kind: String, sub_kind: Option[String]) {
     override def toString = kind
   }
@@ -35,8 +27,7 @@
 
   case class State(
     val command: Command,
-    val status: Command.Status.Value,
-    val forks: Int,
+    val status: List[Markup],
     val reverse_results: List[XML.Tree],
     val markup: Markup_Text)
   {
@@ -90,15 +81,7 @@
     def accumulate(message: XML.Tree): Command.State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), elems) =>
-          (this /: elems)((state, elem) =>
-            elem match {
-              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
-              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
-              case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
-              case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
-              case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
-              case _ => System.err.println("Ignored status message: " + elem); state
-            })
+          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
 
         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
           (this /: elems)((state, elem) =>
@@ -184,6 +167,5 @@
 
   /* accumulated results */
 
-  val empty_state: Command.State =
-    Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
+  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
 }