equal
deleted
inserted
replaced
317 (this /: msgs)((state, msg) => |
317 (this /: msgs)((state, msg) => |
318 msg match { |
318 msg match { |
319 case elem @ XML.Elem(markup, Nil) => |
319 case elem @ XML.Elem(markup, Nil) => |
320 state. |
320 state. |
321 add_status(markup). |
321 add_status(markup). |
322 add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem)) |
322 add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) |
323 case _ => |
323 case _ => |
324 Output.warning("Ignored status message: " + msg) |
324 Output.warning("Ignored status message: " + msg) |
325 state |
325 state |
326 }) |
326 }) |
327 |
327 |
353 state |
353 state |
354 } |
354 } |
355 |
355 |
356 case XML.Elem(Markup(name, atts), args) |
356 case XML.Elem(Markup(name, atts), args) |
357 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
357 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
358 val range = command.proper_range |
358 val range = command.core_range |
359 val props = Position.purge(atts) |
359 val props = Position.purge(atts) |
360 val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) |
360 val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) |
361 state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem)) |
361 state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem)) |
362 |
362 |
363 case _ => bad(); state |
363 case _ => bad(); state |
601 yield Symbol.Text_Chunk.File(name.node) -> file)).toMap |
601 yield Symbol.Text_Chunk.File(name.node) -> file)).toMap |
602 |
602 |
603 def length: Int = source.length |
603 def length: Int = source.length |
604 def range: Text.Range = chunk.range |
604 def range: Text.Range = chunk.range |
605 |
605 |
606 val proper_range: Text.Range = |
606 val core_range: Text.Range = |
607 Text.Range(0, |
607 Text.Range(0, |
608 (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) |
608 (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) |
609 |
609 |
610 def source(range: Text.Range): String = range.substring(source) |
610 def source(range: Text.Range): String = range.substring(source) |
611 |
611 |