src/Pure/PIDE/protocol.scala
changeset 50450 358b6020f8b6
parent 50201 c26369c9eda6
child 50498 6647ba2775c1
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Dec 10 10:41:29 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Dec 10 13:52:33 2012 +0100
     1.3 @@ -118,10 +118,12 @@
     1.4  
     1.5    /* result messages */
     1.6  
     1.7 +  private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
     1.8 +
     1.9    def clean_message(body: XML.Body): XML.Body =
    1.10      body filter {
    1.11 -      case XML.Elem(Markup(Markup.REPORT, _), _) => false
    1.12 -      case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
    1.13 +      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
    1.14 +      case XML.Elem(Markup(name, _), _) => !clean(name)
    1.15        case _ => true
    1.16      } map {
    1.17        case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    1.18 @@ -131,6 +133,8 @@
    1.19  
    1.20    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    1.21      body flatMap {
    1.22 +      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    1.23 +        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    1.24        case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    1.25          List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
    1.26        case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)