1/*  Title:      Pure/PIDE/protocol_message.scala
2    Author:     Makarius
3
4Auxiliary operations on protocol messages.
5*/
6
7package isabelle
8
9
10object 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}
85