author | wenzelm |
Sat, 01 Oct 2022 16:07:05 +0200 (2022-10-01) | |
changeset 76234 | 035ffcd82fb2 |
parent 76233 | f3b23f4eaaac |
child 76235 | 16c12979c132 |
--- a/src/Pure/PIDE/command.scala Sat Oct 01 15:42:52 2022 +0200 +++ b/src/Pure/PIDE/command.scala Sat Oct 01 16:07:05 2022 +0200 @@ -553,7 +553,7 @@ val core_range: Text.Range = Text.Range(0, - span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length)) + span.content.reverseIterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source)