diff -r 094d96f05cba -r 405ccae51c72 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Thu Oct 16 21:38:26 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Fri Oct 17 11:03:16 2025 +0200
@@ -39,8 +39,6 @@
     type Entry = (Symbol.Offset, Time)
     val empty: Command_Timings =
       new Command_Timings(SortedMap.empty, Time.zero)
-    def make(args: IterableOnce[Entry]): Command_Timings =
-      args.iterator.foldLeft(empty)(_ + _)
     def merge(args: IterableOnce[Command_Timings]): Command_Timings =
       args.iterator.foldLeft(empty)(_ ++ _)
   }