src/Pure/PIDE/isar_document.scala
changeset 38581 d503a0912e14
parent 38567 b670faa807c9
child 38887 1261481ef5e5
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Aug 22 19:55:41 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Aug 22 20:11:17 2010 +0200
     1.3 @@ -42,18 +42,16 @@
     1.4    case object Finished extends Status
     1.5    case object Failed extends Status
     1.6  
     1.7 -  def command_status(markup: XML.Body): Status =
     1.8 +  def command_status(markup: List[Markup]): Status =
     1.9    {
    1.10      val forks = (0 /: markup) {
    1.11 -      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
    1.12 -      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
    1.13 +      case (i, Markup(Markup.FORKED, _)) => i + 1
    1.14 +      case (i, Markup(Markup.JOINED, _)) => i - 1
    1.15        case (i, _) => i
    1.16      }
    1.17      if (forks != 0) Forked(forks)
    1.18 -    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
    1.19 -      Failed
    1.20 -    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
    1.21 -      Finished
    1.22 +    else if (markup.exists(_.name == Markup.FAILED)) Failed
    1.23 +    else if (markup.exists(_.name == Markup.FINISHED)) Finished
    1.24      else Unprocessed
    1.25    }
    1.26  }