--- 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
}
}