src/Pure/PIDE/command.scala
changeset 38714 31da698fc4e5
parent 38658 20d82e98bcd7
child 38722 ba31936497c2
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 25 17:45:35 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 25 18:19:04 2010 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4  
     1.5      lazy val results = reverse_results.reverse
     1.6  
     1.7 +    def add_status(st: Markup): State = copy(status = st :: status)
     1.8 +    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
     1.9      def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    1.10  
    1.11 -    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
    1.12 -
    1.13      def root_info: Text.Info[Any] =
    1.14        new Text.Info(command.range,
    1.15          XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    1.16 @@ -36,8 +36,12 @@
    1.17  
    1.18      def accumulate(message: XML.Tree): Command.State =
    1.19        message match {
    1.20 -        case XML.Elem(Markup(Markup.STATUS, _), body) =>  // FIXME explicit body check!?
    1.21 -          copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
    1.22 +        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    1.23 +          (this /: msgs)((state, msg) =>
    1.24 +            msg match {
    1.25 +              case XML.Elem(markup, Nil) => state.add_status(markup)
    1.26 +              case _ => System.err.println("Ignored status message: " + msg); state
    1.27 +            })
    1.28  
    1.29          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    1.30            (this /: msgs)((state, msg) =>
    1.31 @@ -47,7 +51,7 @@
    1.32                  val range = command.decode(Position.get_range(atts).get)
    1.33                  val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    1.34                  val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    1.35 -                add_markup(info)
    1.36 +                state.add_markup(info)
    1.37                case _ => System.err.println("Ignored report message: " + msg); state
    1.38              })
    1.39          case _ => add_result(message)