src/Pure/PIDE/protocol_message.scala
changeset 80872 320bcbf34849
parent 80871 b71a040ab128
child 81414 ed4ff84e9b21
equal deleted inserted replaced
80871:b71a040ab128 80872:320bcbf34849
    41   val any_report_elements: Markup.Elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    41   val any_report_elements: Markup.Elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    42 
    42 
    43   def clean_reports(body: XML.Body): XML.Body =
    43   def clean_reports(body: XML.Body): XML.Body =
    44     XML.filter_elements(body, remove = any_report_elements)
    44     XML.filter_elements(body, remove = any_report_elements)
    45 
    45 
    46   def expose_no_reports(body: XML.Body): XML.Body =
       
    47     XML.filter_elements(body, expose = no_report_elements)
       
    48 
       
    49   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    46   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    50     body flatMap {
    47     body flatMap {
    51       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    48       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    52         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    49         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    53       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    50       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>