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