# HG changeset patch
# User wenzelm
# Date 1664633225 -7200
# Node ID 035ffcd82fb2c5cff2fdee4d17e013042a51cab2
# Parent  f3b23f4eaaac8b990f3a20d8d4c3eac3304d5435
tuned, following hints by IntelliJ IDEA;

diff -r f3b23f4eaaac -r 035ffcd82fb2 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)