# HG changeset patch
# User wenzelm
# Date 1757948276 -7200
# Node ID bc502885f201bcd5f7c5f116ca52db4a0cb99781
# Parent  d5715946bc3f5680e5a48cf68f443dc47158f372
clarified signature;

diff -r d5715946bc3f -r bc502885f201 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Mon Sep 15 16:57:39 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Sep 15 16:57:56 2025 +0200
@@ -194,7 +194,7 @@
   /* overall timing */
 
   object Overall_Timing {
-    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
+    val empty: Overall_Timing = Overall_Timing()
 
     def make(
       state: Document.State,
@@ -218,11 +218,14 @@
           command_timings += (command -> command_timing)
         }
       }
-      Overall_Timing(total, command_timings)
+      Overall_Timing(total = total, command_timings = command_timings)
     }
   }
 
-  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double]) {
+  sealed case class Overall_Timing(
+    total: Double = 0.0,
+    command_timings: Map[Command, Double] = Map.empty
+  ) {
     def command_timing(command: Command): Double =
       command_timings.getOrElse(command, 0.0)
   }