diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -74,7 +74,7 @@
     def keyword_pos(start: Token.Pos): Token.Pos =
       kind match {
         case _: Command_Span =>
-          (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
+          content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_))
         case _ => start
       }
 
@@ -89,7 +89,7 @@
 
     def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
 
-    def length: Int = (0 /: content)(_ + _.source.length)
+    def length: Int = content.foldLeft(0)(_ + _.source.length)
 
     def compact_source: (String, Span) =
     {