--- 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 ->
--- 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)
}
--- 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
}
--- 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(
--- 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
--- 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,
--- 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
}
}
--- 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 ""
}
--- 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,
--- 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)))
}
}
--- 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)) =>
--- 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
}