src/Pure/PIDE/command.scala
changeset 68728 c07f6fa02c59
parent 68381 2fd3a6d6ba2e
child 68729 3a02b424d5fb
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Jul 29 13:18:10 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4                case elem @ XML.Elem(markup, Nil) =>
     1.5                  state.
     1.6                    add_status(markup).
     1.7 -                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
     1.8 +                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
     1.9                case _ =>
    1.10                  Output.warning("Ignored status message: " + msg)
    1.11                  state
    1.12 @@ -355,7 +355,7 @@
    1.13  
    1.14                  case XML.Elem(Markup(name, atts), args)
    1.15                  if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
    1.16 -                  val range = command.proper_range
    1.17 +                  val range = command.core_range
    1.18                    val props = Position.purge(atts)
    1.19                    val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
    1.20                    state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
    1.21 @@ -603,7 +603,7 @@
    1.22    def length: Int = source.length
    1.23    def range: Text.Range = chunk.range
    1.24  
    1.25 -  val proper_range: Text.Range =
    1.26 +  val core_range: Text.Range =
    1.27      Text.Range(0,
    1.28        (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    1.29