src/Pure/PIDE/command.scala
changeset 68729 3a02b424d5fb
parent 68728 c07f6fa02c59
child 68758 a110e7e24e55
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -605,7 +605,7 @@
     1.4  
     1.5    val core_range: Text.Range =
     1.6      Text.Range(0,
     1.7 -      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
     1.8 +      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
     1.9  
    1.10    def source(range: Text.Range): String = range.substring(source)
    1.11