simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
authorwenzelm
Sun Aug 22 20:11:17 2010 +0200 (2010-08-22 ago)
changeset 38581d503a0912e14
parent 38580 881c362d48e4
child 38582 3a6ce43d99b1
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
src/Pure/PIDE/command.scala
src/Pure/PIDE/isar_document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 22 19:55:41 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 22 20:11:17 2010 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5    case class State(
     1.6      val command: Command,
     1.7 -    val status: List[XML.Tree],
     1.8 +    val status: List[Markup],
     1.9      val reverse_results: List[XML.Tree],
    1.10      val markup: Markup_Tree)
    1.11    {
    1.12 @@ -31,7 +31,8 @@
    1.13      def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
    1.14  
    1.15      def markup_root_info: Text.Info[Any] =
    1.16 -      new Text.Info(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
    1.17 +      new Text.Info(command.range,
    1.18 +        XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
    1.19      def markup_root: Markup_Tree = markup + markup_root_info
    1.20  
    1.21  
    1.22 @@ -39,7 +40,9 @@
    1.23  
    1.24      def accumulate(message: XML.Tree): Command.State =
    1.25        message match {
    1.26 -        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
    1.27 +        case XML.Elem(Markup(Markup.STATUS, _), body) =>  // FIXME explicit checks!?
    1.28 +          copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
    1.29 +
    1.30          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    1.31            (this /: msgs)((state, msg) =>
    1.32              msg match {
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Aug 22 19:55:41 2010 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Aug 22 20:11:17 2010 +0200
     2.3 @@ -42,18 +42,16 @@
     2.4    case object Finished extends Status
     2.5    case object Failed extends Status
     2.6  
     2.7 -  def command_status(markup: XML.Body): Status =
     2.8 +  def command_status(markup: List[Markup]): Status =
     2.9    {
    2.10      val forks = (0 /: markup) {
    2.11 -      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
    2.12 -      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
    2.13 +      case (i, Markup(Markup.FORKED, _)) => i + 1
    2.14 +      case (i, Markup(Markup.JOINED, _)) => i - 1
    2.15        case (i, _) => i
    2.16      }
    2.17      if (forks != 0) Forked(forks)
    2.18 -    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
    2.19 -      Failed
    2.20 -    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
    2.21 -      Finished
    2.22 +    else if (markup.exists(_.name == Markup.FAILED)) Failed
    2.23 +    else if (markup.exists(_.name == Markup.FINISHED)) Finished
    2.24      else Unprocessed
    2.25    }
    2.26  }