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