src/Pure/PIDE/protocol.scala
changeset 55646 ec4651c697e3
parent 55548 a645277885cf
child 55783 da0513d95155
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Feb 21 12:07:38 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Feb 21 12:32:06 2014 +0100
     1.3 @@ -63,10 +63,6 @@
     1.4      def is_failed: Boolean = failed
     1.5    }
     1.6  
     1.7 -  val command_status_markup: Set[String] =
     1.8 -    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     1.9 -      Markup.FINISHED, Markup.FAILED)
    1.10 -
    1.11    def command_status(status: Status, markup: Markup): Status =
    1.12      markup match {
    1.13        case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
    1.14 @@ -81,6 +77,13 @@
    1.15    def command_status(markups: List[Markup]): Status =
    1.16      (Status.init /: markups)(command_status(_, _))
    1.17  
    1.18 +  val command_status_elements: Set[String] =
    1.19 +    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    1.20 +      Markup.FINISHED, Markup.FAILED)
    1.21 +
    1.22 +  val status_elements: Set[String] =
    1.23 +    command_status_elements + Markup.WARNING + Markup.ERROR
    1.24 +
    1.25  
    1.26    /* command timing */
    1.27  
    1.28 @@ -162,12 +165,12 @@
    1.29  
    1.30    /* result messages */
    1.31  
    1.32 -  private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
    1.33 +  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
    1.34  
    1.35    def clean_message(body: XML.Body): XML.Body =
    1.36      body filter {
    1.37 -      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
    1.38 -      case XML.Elem(Markup(name, _), _) => !clean(name)
    1.39 +      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
    1.40 +      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
    1.41        case _ => true
    1.42      } map {
    1.43        case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    1.44 @@ -272,7 +275,8 @@
    1.45  
    1.46    /* reported positions */
    1.47  
    1.48 -  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.49 +  private val position_elements =
    1.50 +    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.51  
    1.52    def message_positions(
    1.53      command_id: Document_ID.Command,
    1.54 @@ -294,9 +298,9 @@
    1.55      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.56        tree match {
    1.57          case XML.Wrapped_Elem(Markup(name, props), _, body) =>
    1.58 -          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
    1.59 +          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
    1.60          case XML.Elem(Markup(name, props), body) =>
    1.61 -          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
    1.62 +          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
    1.63          case XML.Text(_) => set
    1.64        }
    1.65