# HG changeset patch # User wenzelm # Date 1614869968 -3600 # Node ID dde25151c3c170e90308ab43867054c5cff62bd5 # Parent ef8c9b3d53558afeaf36181303b646b7ef84606d tuned --- fewer warnings; diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/General/linear_set.scala --- 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]] diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/General/multi_map.scala --- 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]] diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/General/scan.scala --- 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 diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/PIDE/command.scala --- 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]) diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/library.scala --- 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 =