src/Pure/PIDE/protocol_message.scala
changeset 80816 774e5a0c4c9e
parent 80455 99e276c44121
child 80817 e31ebb2be437
equal deleted inserted replaced
80815:cd10c7c9f25c 80816:774e5a0c4c9e
    34   }
    34   }
    35 
    35 
    36 
    36 
    37   /* inlined reports */
    37   /* inlined reports */
    38 
    38 
    39   private val report_elements =
    39   private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    40     Markup.Elements(Markup.REPORT, 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     body filter {
    43     XML.clean_elements(report_elements, body, full = true)
    44       case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
       
    45       case XML.Elem(Markup(name, _), _) => !report_elements(name)
       
    46       case _ => true
       
    47     } map {
       
    48       case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
       
    49       case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
       
    50       case t => t
       
    51     }
       
    52 
    44 
    53   def expose_no_reports(body: XML.Body): XML.Body =
    45   def expose_no_reports(body: XML.Body): XML.Body =
    54     body flatMap {
    46     XML.clean_elements(no_report_elements, body)
    55       case XML.Wrapped_Elem(markup, body, ts) => List(XML.Wrapped_Elem(markup, body, expose_no_reports(ts)))
       
    56       case XML.Elem(Markup(Markup.NO_REPORT, _), ts) => ts
       
    57       case XML.Elem(markup, ts) => List(XML.Elem(markup, expose_no_reports(ts)))
       
    58       case t => List(t)
       
    59     }
       
    60 
    47 
    61   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    48   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    62     body flatMap {
    49     body flatMap {
    63       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    50       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    64         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    51         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))