# HG changeset patch
# User wenzelm
# Date 1614637067 -3600
# Node ID f5c1476546613b89fd885560afd41413ed09287f
# Parent  d0378baf7d067ddf9b0bf7022b77f1b5b406c381
tuned --- fewer warnings;

diff -r d0378baf7d06 -r f5c147654661 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -1099,7 +1099,7 @@
       db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
       {
         val res = stmt.execute_query()
-        if (!res.next) None
+        if (!res.next()) None
         else {
           val results =
             columns.map(c => c.name ->
diff -r d0378baf7d06 -r f5c147654661 src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/General/untyped.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -47,7 +47,7 @@
         field.setAccessible(true)
         field
       }
-    if (iterator.hasNext) iterator.next
+    if (iterator.hasNext) iterator.next()
     else error("No field " + quote(x) + " for " + obj)
   }
 
diff -r d0378baf7d06 -r f5c147654661 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/General/word.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -57,7 +57,7 @@
         else if (Codepoint.iterator(str).forall(Character.isUpperCase)) Some(Uppercase)
         else {
           val it = Codepoint.iterator(str)
-          if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase))
+          if (Character.isUpperCase(it.next()) && it.forall(Character.isLowerCase))
             Some(Capitalized)
           else None
         }
diff -r d0378baf7d06 -r f5c147654661 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -692,7 +692,7 @@
         val other_node = get_node(other_node_name)
         val iterator = other_node.command_iterator(revert(offset) max 0)
         if (iterator.hasNext) {
-          val (command0, _) = iterator.next
+          val (command0, _) = iterator.next()
           other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
         }
         else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
@@ -1231,7 +1231,7 @@
       !name.is_theory ||
       {
         val it = version.nodes(name).commands.reverse.iterator
-        it.hasNext && command_states(version, it.next).exists(_.consolidated)
+        it.hasNext && command_states(version, it.next()).exists(_.consolidated)
       }
 
     def snapshot(
diff -r d0378baf7d06 -r f5c147654661 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -59,7 +59,7 @@
 
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {
-        val status0 = status_iterator.next
+        val status0 = status_iterator.next()
         (status0 /: status_iterator)(_ + _)
       }
       else empty
diff -r d0378baf7d06 -r f5c147654661 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -275,7 +275,7 @@
                       var last = last_visible
                       var i = 0
                       while (i < reparse_limit && it.hasNext) {
-                        last = it.next
+                        last = it.next()
                         i += last.length
                       }
                       reparse_spans(resources, syntax, get_blob, can_import,
diff -r d0378baf7d06 -r f5c147654661 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -142,7 +142,7 @@
         skip(name)
           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
           || !graph.is_minimal(name))
-      if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
+      if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }
   }
diff -r d0378baf7d06 -r f5c147654661 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -108,7 +108,7 @@
   def first_line(source: CharSequence): String =
   {
     val lines = separated_chunks(_ == '\n', source)
-    if (lines.hasNext) lines.next.toString
+    if (lines.hasNext) lines.next().toString
     else ""
   }
 
diff -r d0378baf7d06 -r f5c147654661 src/Tools/Graphview/mutator.scala
--- a/src/Tools/Graphview/mutator.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Tools/Graphview/mutator.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -19,7 +19,7 @@
   sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator)
 
   def make(graphview: Graphview, m: Mutator): Info =
-    Info(true, graphview.Colors.next, m)
+    Info(true, graphview.Colors.next(), m)
 
   class Graph_Filter(
     val name: String,
diff -r d0378baf7d06 -r f5c147654661 src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -117,7 +117,7 @@
   private val add_button = new Button {
     action = Action("Add") {
       add_panel(
-        new Mutator_Panel(Mutator.Info(true, graphview.Colors.next, mutator_box.selection.item)))
+        new Mutator_Panel(Mutator.Info(true, graphview.Colors.next(), mutator_box.selection.item)))
     }
   }
 
diff -r d0378baf7d06 -r f5c147654661 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -221,7 +221,7 @@
       restrict: Token => Boolean,
       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
     {
-      val range1 = it.next.range
+      val range1 = it.next().range
       it.takeWhile(info => !info.info.is_command || restrict(info.info)).
         scanLeft((range1, 1))(
           { case ((r, d), Text.Info(range, tok)) =>
diff -r d0378baf7d06 -r f5c147654661 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -196,7 +196,7 @@
       def hasNext: Boolean = next_span.isDefined
       def next(): Text.Info[Command_Span.Span] =
       {
-        val span = next_span.getOrElse(Iterator.empty.next)
+        val span = next_span.getOrElse(Iterator.empty.next())
         next_span = command_span(syntax, buffer, next_offset(span.range))
         span
       }