# HG changeset patch
# User wenzelm
# Date 1758134188 -7200
# Node ID 5e2076fb2eff0a49a3f5f07d4ed19fe6d4d540a6
# Parent  481c3e1cb957622027b3cbdd9d349101cad63fb9
more informative Node_Status;

diff -r 481c3e1cb957 -r 5e2076fb2eff src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Wed Sep 17 20:13:18 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 17 20:36:28 2025 +0200
@@ -191,6 +191,7 @@
       var canceled = false
       var terminated = true
       var total_time = Time.zero
+      var max_time = Time.zero
       var command_timings = Map.empty[Command, Time]
       var theory_status = Document_Status.Theory_Status.NONE
 
@@ -208,6 +209,7 @@
 
         val t = state.command_timing(version, command).elapsed
         total_time += t
+        if (t > max_time) max_time = t
         if (t.is_notable(threshold)) command_timings += (command -> t)
 
         theory_status = Theory_Status.merge(theory_status, status.theory_status)
@@ -223,6 +225,7 @@
         canceled = canceled,
         terminated = terminated,
         total_time = total_time,
+        max_time = max_time,
         threshold = threshold,
         command_timings = command_timings,
         theory_status = theory_status)
@@ -239,6 +242,7 @@
     canceled: Boolean = false,
     terminated: Boolean = false,
     total_time: Time = Time.zero,
+    max_time: Time = Time.zero,
     threshold: Time = Time.zero,
     command_timings: Map[Command, Time] = Map.empty,
     theory_status: Theory_Status.Value = Theory_Status.NONE,