# HG changeset patch
# User wenzelm
# Date 1614807071 -3600
# Node ID 31d4274f32de27975fd5a038df14418a75123f8b
# Parent  819f6033fb4ee0074253023484866399e28070d9
tuned --- fewer warnings;

diff -r 819f6033fb4e -r 31d4274f32de src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Pure/General/scan.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -8,7 +8,7 @@
 
 
 import scala.annotation.tailrec
-import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
+import scala.collection.IndexedSeq
 import scala.util.matching.Regex
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
   Reader, CharSequenceReader, PagedSeq}
@@ -390,14 +390,14 @@
         new Lexicon(extend(rep, 0))
       }
 
-    def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
+    def ++ (elems: IterableOnce[String]): Lexicon = (this /: elems)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this
       else if (is_empty) other
       else this ++ other.raw_iterator
 
-    def -- (remove: Traversable[String]): Lexicon =
+    def -- (remove: Iterable[String]): Lexicon =
       if (remove.exists(contains))
         Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
       else this
diff -r 819f6033fb4e -r 31d4274f32de src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -56,8 +56,8 @@
   {
     type Entry = (Long, XML.Elem)
     val empty: Results = new Results(SortedMap.empty)
-    def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
-    def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
+    def make(args: IterableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
+    def merge(args: IterableOnce[Results]): Results = (empty /: args)(_ ++ _)
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Elem])
@@ -92,7 +92,7 @@
   {
     type Entry = (Long, Export.Entry)
     val empty: Exports = new Exports(SortedMap.empty)
-    def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
+    def merge(args: IterableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
   }
 
   final class Exports private(private val rep: SortedMap[Long, Export.Entry])
@@ -134,8 +134,8 @@
     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: TraversableOnce[Entry]): Markups = (empty /: args)(_ + _)
-    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
+    def make(args: IterableOnce[Entry]): Markups = (empty /: args)(_ + _)
+    def merge(args: IterableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
diff -r 819f6033fb4e -r 31d4274f32de src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -644,7 +644,7 @@
 
     def make(infos: List[Info]): Structure =
     {
-      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
+      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Iterable[String])
         : Graph[String, Info] =
       {
         def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
diff -r 819f6033fb4e -r 31d4274f32de src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Pure/library.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -96,9 +96,9 @@
 
   /* lines */
 
-  def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
+  def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n")
 
-  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
+  def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
@@ -126,7 +126,7 @@
 
   /* strings */
 
-  def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000")
+  def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000")
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =
diff -r 819f6033fb4e -r 31d4274f32de src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -352,7 +352,7 @@
     private var items = Vector.empty[java.awt.Component]
 
     def add(c: java.awt.Component): Unit = { items = items :+ c }
-    def addAll(cs: TraversableOnce[java.awt.Component]): Unit = { items = items ++ cs }
+    def addAll(cs: IterableOnce[java.awt.Component]): Unit = { items = items ++ cs }
     def clear(): Unit = { items = Vector.empty }
 
     def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
diff -r 819f6033fb4e -r 31d4274f32de src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -221,7 +221,7 @@
       if (resources.flush_output(channel)) delay_output.invoke()
     }
 
-  def update_output(changed_nodes: Traversable[JFile]): Unit =
+  def update_output(changed_nodes: Iterable[JFile]): Unit =
   {
     resources.update_output(changed_nodes)
     delay_output.invoke()
diff -r 819f6033fb4e -r 31d4274f32de src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Mar 03 22:28:03 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Mar 03 22:31:11 2021 +0100
@@ -25,7 +25,7 @@
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
   {
-    def update_models(changed: Traversable[(JFile, VSCode_Model)]): State =
+    def update_models(changed: Iterable[(JFile, VSCode_Model)]): State =
       copy(
         models = models ++ changed,
         pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
@@ -293,7 +293,7 @@
 
   /* pending output */
 
-  def update_output(changed_nodes: Traversable[JFile]): Unit =
+  def update_output(changed_nodes: Iterable[JFile]): Unit =
     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
 
   def update_output_visible(): Unit =