src/Pure/PIDE/document_status.scala

 
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
     def make(
-      markups: Iterable[Markup],
+      markups: Iterable[Markup] = Nil,
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
       var theory_status = Theory_Status.NONE
       var touched = false

         canceled = canceled,
         forks = forks,
         runs = runs)
     }
 
-    val empty: Command_Status = make(Nil)
+    val empty: Command_Status = make()
 
     def merge(args: IterableOnce[Command_Status]): Command_Status =
       args.iterator.foldLeft(empty)(_ + _)
   }