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