src/Pure/PIDE/command.scala

 import scala.collection.mutable
 
 
 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
   }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],

 
   /** accumulated results from prover **/
 
   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)
   {
     /* content */
 

     /* message dispatch */
 
     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) =>
             elem match {
               case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>

   }
 
 
   /* 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))
 }