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)