tuned --- fewer warnings;

--- a/src/Pure/General/linear_set.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/General/linear_set.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -18,7 +18,8 @@
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
   override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
-  def from[A](entries: IterableOnce[A]): Linear_Set[A] = entries.foldLeft(empty[A])(_.incl(_))
+  def from[A](entries: IterableOnce[A]): Linear_Set[A] =
+    entries.iterator.foldLeft(empty[A])(_.incl(_))
 
   override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
   private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]

--- a/src/Pure/General/multi_map.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/General/multi_map.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -17,7 +17,7 @@
   def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
 
   def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] =
-    entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) }
+    entries.iterator.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) }
 
   override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B]
   private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]

--- a/src/Pure/General/scan.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/General/scan.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -390,7 +390,8 @@
         new Lexicon(extend(rep, 0))
       }
 
-    def ++ (elems: IterableOnce[String]): Lexicon = elems.foldLeft(this)(_ + _)
+    def ++ (elems: IterableOnce[String]): Lexicon =
+      elems.iterator.foldLeft(this)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this

--- a/src/Pure/PIDE/command.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -56,8 +56,10 @@
   {
     type Entry = (Long, XML.Elem)
     val empty: Results = new Results(SortedMap.empty)
-    def make(args: IterableOnce[Results.Entry]): Results = args.foldLeft(empty)(_ + _)
-    def merge(args: IterableOnce[Results]): Results = args.foldLeft(empty)(_ ++ _)
+    def make(args: IterableOnce[Results.Entry]): Results =
+      args.iterator.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Results]): Results =
+      args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem])
@@ -92,7 +94,8 @@
   {
     type Entry = (Long, Export.Entry)
     val empty: Exports = new Exports(SortedMap.empty)
-    def merge(args: IterableOnce[Exports]): Exports = args.foldLeft(empty)(_ ++ _)
+    def merge(args: IterableOnce[Exports]): Exports =
+      args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry])
@@ -134,8 +137,10 @@
     type Entry = (Markup_Index, Markup_Tree)
     val empty: Markups = new Markups(Map.empty)
     def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
-    def make(args: IterableOnce[Entry]): Markups = args.foldLeft(empty)(_ + _)
-    def merge(args: IterableOnce[Markups]): Markups = args.foldLeft(empty)(_ ++ _)
+    def make(args: IterableOnce[Entry]): Markups =
+      args.iterator.foldLeft(empty)(_ + _)
+    def merge(args: IterableOnce[Markups]): Markups =
+      args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])

--- a/src/Pure/library.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/library.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -96,9 +96,11 @@
 
   /* lines */
 
-  def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n")
+  def terminate_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("", "\n", "\n")
 
-  def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n")
+  def cat_lines(lines: IterableOnce[String]): String =
+    lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
@@ -126,7 +128,9 @@
 
   /* strings */
 
-  def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000")
+  def cat_strings0(strs: IterableOnce[String]): String =
+    strs.iterator.mkString("\u0000")
+
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =