src/Pure/PIDE/protocol_message.scala
changeset 80818 da2557168da7
parent 80817 e31ebb2be437
child 80819 84e886792536
equal deleted inserted replaced
80817:e31ebb2be437 80818:da2557168da7
    38 
    38 
    39   private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    39   private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    40   private val no_report_elements = Markup.Elements(Markup.NO_REPORT)
    40   private val no_report_elements = Markup.Elements(Markup.NO_REPORT)
    41 
    41 
    42   def clean_reports(body: XML.Body): XML.Body =
    42   def clean_reports(body: XML.Body): XML.Body =
    43     XML.clean_elements(report_elements, body, full = true)
    43     XML.filter_elements(body, remove = report_elements)
    44 
    44 
    45   def expose_no_reports(body: XML.Body): XML.Body =
    45   def expose_no_reports(body: XML.Body): XML.Body =
    46     XML.clean_elements(no_report_elements, body)
    46     XML.filter_elements(body, expose = no_report_elements)
    47 
    47 
    48   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    48   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    49     body flatMap {
    49     body flatMap {
    50       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    50       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    51         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    51         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))