# HG changeset patch
# User wenzelm
# Date 1282500677 -7200
# Node ID d503a0912e1419ce8866fb63e3bb2ad5fcacbfd1
# Parent  881c362d48e41bfa446c1bc32dc5ccfa322d46a2
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

diff -r 881c362d48e4 -r d503a0912e14 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Aug 22 19:55:41 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 22 20:11:17 2010 +0200
@@ -18,7 +18,7 @@
 
   case class State(
     val command: Command,
-    val status: List[XML.Tree],
+    val status: List[Markup],
     val reverse_results: List[XML.Tree],
     val markup: Markup_Tree)
   {
@@ -31,7 +31,8 @@
     def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
 
     def markup_root_info: Text.Info[Any] =
-      new Text.Info(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
+      new Text.Info(command.range,
+        XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
     def markup_root: Markup_Tree = markup + markup_root_info
 
 
@@ -39,7 +40,9 @@
 
     def accumulate(message: XML.Tree): Command.State =
       message match {
-        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
+        case XML.Elem(Markup(Markup.STATUS, _), body) =>  // FIXME explicit checks!?
+          copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
+
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
diff -r 881c362d48e4 -r d503a0912e14 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sun Aug 22 19:55:41 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Aug 22 20:11:17 2010 +0200
@@ -42,18 +42,16 @@
   case object Finished extends Status
   case object Failed extends Status
 
-  def command_status(markup: XML.Body): Status =
+  def command_status(markup: List[Markup]): Status =
   {
     val forks = (0 /: markup) {
-      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
-      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
+      case (i, Markup(Markup.FORKED, _)) => i + 1
+      case (i, Markup(Markup.JOINED, _)) => i - 1
       case (i, _) => i
     }
     if (forks != 0) Forked(forks)
-    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
-      Failed
-    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
-      Finished
+    else if (markup.exists(_.name == Markup.FAILED)) Failed
+    else if (markup.exists(_.name == Markup.FINISHED)) Finished
     else Unprocessed
   }
 }