diff -r 2472024d9a1c -r 6e03fb945baf src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 20:33:36 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 21:04:39 2025 +0200
@@ -41,7 +41,7 @@
       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 = {
@@ -85,7 +85,7 @@
         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)(_ + _)