# HG changeset patch
# User wenzelm
# Date 1282209967 -7200
# Node ID e5eed57913d0545af276e7affbbc5e828e6ebeb0
# Parent  e628da370072599a9c4c8c37a2f5f8ab8851133b
Command.status: full XML.Tree, i.e. Markup with potential "arguments";

diff -r e628da370072 -r e5eed57913d0 src/Pure/Isar/toplevel.scala
--- a/src/Pure/Isar/toplevel.scala	Wed Aug 18 23:44:50 2010 +0200
+++ b/src/Pure/Isar/toplevel.scala	Thu Aug 19 11:26:07 2010 +0200
@@ -15,16 +15,18 @@
   case object Finished extends Status
   case object Failed extends Status
 
-  def command_status(markup: List[Markup]): Status =
+  def command_status(markup: XML.Body): Status =
   {
     val forks = (0 /: markup) {
-      case (i, Markup(Markup.FORKED, _)) => i + 1
-      case (i, Markup(Markup.JOINED, _)) => i - 1
+      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
+      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
       case (i, _) => i
     }
     if (forks != 0) Forked(forks)
-    else if (markup.exists(_.name == Markup.FAILED)) Failed
-    else if (markup.exists(_.name == Markup.FINISHED)) Finished
+    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 Unprocessed
   }
 }
diff -r e628da370072 -r e5eed57913d0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 18 23:44:50 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Aug 19 11:26:07 2010 +0200
@@ -27,7 +27,7 @@
 
   case class State(
     val command: Command,
-    val status: List[Markup],
+    val status: List[XML.Tree],
     val reverse_results: List[XML.Tree],
     val markup: Markup_Tree)
   {
@@ -39,7 +39,8 @@
 
     def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
 
-    def markup_root_node: Markup_Tree.Node = new Markup_Tree.Node(command.range, status)
+    def markup_root_node: Markup_Tree.Node =
+      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
     def markup_root: Markup_Tree = markup + markup_root_node
 
 
@@ -83,8 +84,7 @@
 
     def accumulate(message: XML.Tree): Command.State =
       message match {
-        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
-          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
+        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
 
         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
           (this /: elems)((state, elem) =>