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) =>