tuned, following hints by IntelliJ IDEA;
authorwenzelm
Sat, 01 Oct 2022 16:07:05 +0200 (2022-10-01)
changeset 76234 035ffcd82fb2
parent 76233 f3b23f4eaaac
child 76235 16c12979c132
tuned, following hints by IntelliJ IDEA;
src/Pure/PIDE/command.scala
--- 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)