# HG changeset patch
# User wenzelm
# Date 1614624112 -3600
# Node ID 0af9e7e4476ff9e439df06b6e0565a998a87487b
# Parent  ff7ce802be52824d4da87c5492741586cd5b478a
tuned --- fewer warnings;

diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -251,7 +251,7 @@
 
   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
     private var next_elem = get_parent(component)
-    def hasNext(): Boolean = next_elem.isDefined
+    def hasNext: Boolean = next_elem.isDefined
     def next(): Container =
       next_elem match {
         case Some(parent) =>
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/General/codepoint.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -18,7 +18,7 @@
   {
     var offset = 0
     def hasNext: Boolean = offset < s.length
-    def next: A =
+    def next(): A =
     {
       val c = s.codePointAt(offset)
       val i = offset
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/General/linear_set.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -127,7 +127,7 @@
 
   private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = from
-    def hasNext(): Boolean = next_elem.isDefined
+    def hasNext: Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {
         case Some(elem) =>
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -269,7 +269,7 @@
     {
       private var _next: Boolean = res.next()
       def hasNext: Boolean = _next
-      def next: A = { val x = get(res); _next = res.next(); x }
+      def next(): A = { val x = get(res); _next = res.next(); x }
     }
 
     def bool(column: Column): Boolean = rep.getBoolean(column.name)
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/General/symbol.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -117,7 +117,7 @@
       private val matcher = new Matcher(text)
       private var i = 0
       def hasNext: Boolean = i < text.length
-      def next: Symbol =
+      def next(): Symbol =
       {
         val n = matcher(i, text.length)
         val s =
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/General/untyped.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -28,7 +28,7 @@
 
   def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
     private var next_elem: Class[_ <: AnyRef] = obj.getClass
-    def hasNext(): Boolean = next_elem != null
+    def hasNext: Boolean = next_elem != null
     def next(): Class[_ <: AnyRef] = {
       val c = next_elem
       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
diff -r ff7ce802be52 -r 0af9e7e4476f src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -82,7 +82,7 @@
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
 
-      def hasNext(): Boolean = state.isDefined
+      def hasNext: Boolean = state.isDefined
       def next(): CharSequence =
         state match {
           case Some((s, i)) => state = next_chunk(i); s
diff -r ff7ce802be52 -r 0af9e7e4476f src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -396,7 +396,7 @@
     new Iterator[Layout.Info] {
       private var index = 0
       def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
-      def next: Layout.Info =
+      def next(): Layout.Info =
       {
         val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
         index += 1
diff -r ff7ce802be52 -r 0af9e7e4476f src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -65,8 +65,8 @@
       override lazy val peer = button
       name = opt_name
       val title = opt_title
-      def load = button.setSelectedColor(Color_Value(string(opt_name)))
-      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
+      def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
+      def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
@@ -84,8 +84,8 @@
         new CheckBox with Option_Component {
           name = opt_name
           val title = opt_title
-          def load = selected = bool(opt_name)
-          def save = bool(opt_name) = selected
+          def load(): Unit = selected = bool(opt_name)
+          def save(): Unit = bool(opt_name) = selected
         }
       else {
         val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
@@ -94,8 +94,8 @@
             if (default_font != null) font = default_font
             name = opt_name
             val title = opt_title
-            def load = text = value.check_name(opt_name).value
-            def save =
+            def load(): Unit = text = value.check_name(opt_name).value
+            def save(): Unit =
               try { JEdit_Options.this += (opt_name, text) }
               catch {
                 case ERROR(msg) =>
diff -r ff7ce802be52 -r 0af9e7e4476f src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -94,7 +94,7 @@
     val component = new ComboBox(entries) with Option_Component {
       name = jedit_logic_option
       val title = "Logic"
-      def load: Unit =
+      def load(): Unit =
       {
         val logic = options.string(jedit_logic_option)
         entries.find(_.name == logic) match {
@@ -102,7 +102,7 @@
           case None =>
         }
       }
-      def save: Unit = options.string(jedit_logic_option) = selection.item.name
+      def save(): Unit = options.string(jedit_logic_option) = selection.item.name
     }
 
     component.load()
diff -r ff7ce802be52 -r 0af9e7e4476f src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -91,7 +91,7 @@
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
       val title = opt.title()
-      def load: Unit =
+      def load(): Unit =
       {
         val lang = PIDE.options.string(option_name)
         entries.find(_.lang == lang) match {
@@ -99,7 +99,7 @@
           case None =>
         }
       }
-      def save: Unit = PIDE.options.string(option_name) = selection.item.lang
+      def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
     }
 
     component.load()
diff -r ff7ce802be52 -r 0af9e7e4476f src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Mar 01 18:31:11 2021 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Mar 01 19:41:52 2021 +0100
@@ -194,7 +194,7 @@
     {
       private var next_span = command_span(syntax, buffer, offset)
       def hasNext: Boolean = next_span.isDefined
-      def next: Text.Info[Command_Span.Span] =
+      def next(): Text.Info[Command_Span.Span] =
       {
         val span = next_span.getOrElse(Iterator.empty.next)
         next_span = command_span(syntax, buffer, next_offset(span.range))