diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/document_status.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -55,7 +55,7 @@
         runs = runs)
     }
 
-    val empty = make(Iterator.empty)
+    val empty: Command_Status = make(Iterator.empty)
 
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {