src/Pure/PIDE/protocol_message.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 59713 6da3efec20ca
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     1 /*  Title:      Pure/PIDE/protocol_message.scala
     2     Author:     Makarius
     3 
     4 Auxiliary operations on protocol messages.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Protocol_Message
    11 {
    12   /* inlined reports */
    13 
    14   private val report_elements =
    15     Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    16 
    17   def clean_reports(body: XML.Body): XML.Body =
    18     body filter {
    19       case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
    20       case XML.Elem(Markup(name, _), _) => !report_elements(name)
    21       case _ => true
    22     } map {
    23       case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
    24       case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
    25       case t => t
    26     }
    27 
    28   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    29     body flatMap {
    30       case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
    31         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
    32       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
    33         List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
    34       case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
    35       case XML.Elem(_, ts) => reports(props, ts)
    36       case XML.Text(_) => Nil
    37     }
    38 
    39 
    40   /* reported positions */
    41 
    42   private val position_elements =
    43     Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    44 
    45   def positions(
    46     self_id: Document_ID.Generic => Boolean,
    47     command_position: Position.T,
    48     chunk_name: Symbol.Text_Chunk.Name,
    49     chunk: Symbol.Text_Chunk,
    50     message: XML.Elem): Set[Text.Range] =
    51   {
    52     def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    53       props match {
    54         case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
    55           val opt_range =
    56             Position.Range.unapply(props) orElse {
    57               if (name == Symbol.Text_Chunk.Default)
    58                 Position.Range.unapply(command_position)
    59               else None
    60             }
    61           opt_range match {
    62             case Some(symbol_range) =>
    63               chunk.incorporate(symbol_range) match {
    64                 case Some(range) => set + range
    65                 case _ => set
    66               }
    67             case None => set
    68           }
    69         case _ => set
    70       }
    71     def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
    72       t match {
    73         case XML.Wrapped_Elem(Markup(name, props), _, body) =>
    74           body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
    75         case XML.Elem(Markup(name, props), body) =>
    76           body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
    77         case XML.Text(_) => set
    78       }
    79 
    80     val set = tree(Set.empty, message)
    81     if (set.isEmpty) elem(message.markup.properties, set)
    82     else set
    83   }
    84 }