262 } |
262 } |
263 |
263 |
264 def accumulate( |
264 def accumulate( |
265 self_id: Document_ID.Generic => Boolean, |
265 self_id: Document_ID.Generic => Boolean, |
266 other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], |
266 other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], |
267 message: XML.Elem): State = |
267 message: XML.Elem, |
|
268 xml_cache: XML.Cache): State = |
268 message match { |
269 message match { |
269 case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
270 case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
270 (this /: msgs)((state, msg) => |
271 (this /: msgs)((state, msg) => |
271 msg match { |
272 msg match { |
272 case elem @ XML.Elem(markup, Nil) => |
273 case elem @ XML.Elem(markup, Nil) => |
295 (target, atts) match { |
296 (target, atts) match { |
296 case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => |
297 case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => |
297 target_chunk.incorporate(symbol_range) match { |
298 target_chunk.incorporate(symbol_range) match { |
298 case Some(range) => |
299 case Some(range) => |
299 val props = Position.purge(atts) |
300 val props = Position.purge(atts) |
300 val info = Text.Info(range, XML.Elem(Markup(name, props), args)) |
301 val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) |
301 state.add_markup(false, target_name, info) |
302 state.add_markup(false, target_name, Text.Info(range, elem)) |
302 case None => bad(); state |
303 case None => bad(); state |
303 } |
304 } |
304 case _ => |
305 case _ => |
305 // silently ignore excessive reports |
306 // silently ignore excessive reports |
306 state |
307 state |
308 |
309 |
309 case XML.Elem(Markup(name, atts), args) |
310 case XML.Elem(Markup(name, atts), args) |
310 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
311 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
311 val range = command.proper_range |
312 val range = command.proper_range |
312 val props = Position.purge(atts) |
313 val props = Position.purge(atts) |
313 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
314 val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) |
314 state.add_markup(false, Symbol.Text_Chunk.Default, info) |
315 state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem)) |
315 |
316 |
316 case _ => bad(); state |
317 case _ => bad(); state |
317 } |
318 } |
318 }) |
319 }) |
319 case XML.Elem(Markup(name, props), body) => |
320 case XML.Elem(Markup(name, props), body) => |
320 props match { |
321 props match { |
321 case Markup.Serial(i) => |
322 case Markup.Serial(i) => |
322 val markup_message = XML.Elem(Markup(Markup.message(name), props), body) |
323 val markup_message = |
323 val message_markup = XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))) |
324 xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) |
|
325 val message_markup = |
|
326 xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) |
324 |
327 |
325 var st = copy(results = results + (i -> markup_message)) |
328 var st = copy(results = results + (i -> markup_message)) |
326 if (Protocol.is_inlined(message)) { |
329 if (Protocol.is_inlined(message)) { |
327 for { |
330 for { |
328 (chunk_name, chunk) <- command.chunks.iterator |
331 (chunk_name, chunk) <- command.chunks.iterator |