clarified command_timing protocol: support for still running commands, with timing approximated in Isabelle/Scala;

--- a/src/Pure/General/timing.ML	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/General/timing.ML	Fri Oct 17 15:13:45 2025 +0200
@@ -107,10 +107,17 @@
 
 fun protocol name pos f x =
   let
+    val bs = (Markup.nameN, name) :: Position.properties_of pos;
+    fun message timing =
+      let val a =
+        (case timing of
+          NONE => Markup.command_running
+        | SOME elapsed => (Markup.elapsedN, Time.print elapsed))
+      in Output.try_protocol_message (Markup.command_timing :: a :: bs) [] end;
+
+    val _ = message NONE;
     val ({elapsed, ...}, result) = timing (Exn.result f) x;
-    val props =
-       (Markup.nameN, name) :: (Markup.elapsedN, Time.print elapsed) :: Position.properties_of pos;
-    val _ = Output.try_protocol_message (Markup.command_timing :: props) [];
+    val _ = message (SOME elapsed);
   in Exn.release result end;
 
 end;

--- a/src/Pure/PIDE/command.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -217,7 +217,9 @@
       markups: Markups = Markups.empty,
     ): State = {
       new State(command, results, exports, markups,
-        Document_Status.Command_Status.make(warned = results.warned, failed = results.failed))
+        Document_Status.Command_Status.make(Time.now(),
+          warned = results.warned,
+          failed = results.failed))
     }
   }
 
@@ -250,13 +252,13 @@
       new Command(id, command.node_name, command.blobs_info, command.span, command.source,
         results, exports, markups, document_status)
 
-    private def add_status(st: Markup): State =
+    private def add_status(now: Time, st: Markup): State =
       new State(command, results, exports, markups,
-        document_status.update(markups = List(st)))
+        document_status.update(now, markups = List(st)))
 
-    private def add_result(entry: Results.Entry): State =
+    private def add_result(now: Time, entry: Results.Entry): State =
       new State(command, results + entry, exports, markups,
-        document_status.update(
+        document_status.update(now,
           warned = Results.warned(entry),
           failed = Results.failed(entry)))
 
@@ -280,13 +282,15 @@
     }
 
     def accumulate(
+        now: Time,
         self_id: Document_ID.Generic => Boolean,
         other_id: (Document.Node.Name, Document_ID.Generic) =>
           Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
         message: XML.Elem,
         cache: XML.Cache): State =
       message match {
-        case XML.Elem(markup@Markup(Markup.Command_Timing.name, _), _) => add_status(markup)
+        case XML.Elem(markup@Markup(Markup.Command_Timing.name, _), _) =>
+          add_status(now, markup)
 
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           if (command.span.is_theory) this
@@ -296,7 +300,7 @@
                 msg match {
                   case elem @ XML.Elem(markup, Nil) =>
                     state.
-                      add_status(markup).
+                      add_status(now, markup).
                       add_markup(Text.Info(command.core_range, elem), status = true)
                   case _ =>
                     Output.warning("Ignored status message: " + msg)
@@ -348,7 +352,7 @@
               val markup_message = cache.elem(Protocol.make_message(body, name, props = props))
               val message_markup = cache.elem(XML.elem(Markup(name, Markup.Serial(i))))
 
-              var st = add_result(i -> markup_message)
+              var st = add_result(now, i -> markup_message)
               if (Protocol.is_inlined(message)) {
                 for {
                   (chunk_name, chunk) <- command.chunks.iterator
@@ -619,7 +623,9 @@
 
   lazy val init_state: Command.State =
     new Command.State(this, init_results, init_exports, init_markups,
-      init_document_status.update(warned = init_results.warned, failed = init_results.failed))
+      init_document_status.update(Time.now(),
+        warned = init_results.warned,
+        failed = init_results.failed))
 
   lazy val empty_state: Command.State = Command.State(this)
 }

--- a/src/Pure/PIDE/document.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -1036,8 +1036,9 @@
       message: XML.Elem,
       cache: XML.Cache
     ) : (Command.State, State) = {
+      val now = Time.now()
       def update(st: Command.State): (Command.State, State) = {
-        val st1 = st.accumulate(self_id(st), other_id, message, cache)
+        val st1 = st.accumulate(now, self_id(st), other_id, message, cache)
         (st1, copy(commands_redirection = redirection(st1)))
       }
       execs.get(id).map(update) match {

--- a/src/Pure/PIDE/document_status.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -38,38 +38,49 @@
   object Command_Timings {
     type Entry = (Symbol.Offset, Time)
     val empty: Command_Timings =
-      new Command_Timings(SortedMap.empty, Time.zero)
+      new Command_Timings(SortedMap.empty, SortedMap.empty, Time.zero)
     def merge(args: IterableOnce[Command_Timings]): Command_Timings =
       args.iterator.foldLeft(empty)(_ ++ _)
   }
 
   final class Command_Timings private(
-    private val rep: SortedMap[Symbol.Offset, Time],
-    val sum: Time
+    private val running: SortedMap[Symbol.Offset, Time],  // start time (in Scala)
+    private val finished: SortedMap[Symbol.Offset, Time],  // elapsed time (in ML)
+    private val sum_finished: Time
   ) {
-    def is_empty: Boolean = rep.isEmpty
-    def count: Int = rep.size
-    def apply(offset: Symbol.Offset): Time = rep.getOrElse(offset, Time.zero)
-    def iterator: Iterator[(Symbol.Offset, Time)] = rep.iterator
+    def is_empty: Boolean = running.isEmpty && finished.isEmpty
+
+    def has_running: Boolean = running.nonEmpty
+    def add_running(entry: Command_Timings.Entry): Command_Timings =
+      new Command_Timings(running + entry, finished, sum_finished)
 
-    def + (entry: Command_Timings.Entry): Command_Timings = {
+    def count_finished: Int = finished.size
+    def get_finished(offset: Symbol.Offset): Time = finished.getOrElse(offset, Time.zero)
+    def add_finished(entry: Command_Timings.Entry): Command_Timings = {
       val (offset, t) = entry
-      val rep1 = rep + (offset -> (apply(offset) + t))
-      val sum1 = sum + t
-      new Command_Timings(rep1, sum1)
+      val running1 = running - offset
+      val finished1 = finished + (offset -> (get_finished(offset) + t))
+      val sum_finished1 = sum_finished + t
+      new Command_Timings(running1, finished1, sum_finished1)
     }
 
+    def sum(now: Time): Time =
+      running.valuesIterator.foldLeft(sum_finished)({ case (t, t0) => t + (now - t0) })
+
     def ++ (other: Command_Timings): Command_Timings =
-      if (rep.isEmpty) other
-      else other.rep.foldLeft(this)(_ + _)
+      if (is_empty) other
+      else other.running.foldLeft(other.finished.foldLeft(this)(_ add_finished _))(_ add_running _)
 
-    override def hashCode: Int = rep.hashCode
+
+    override def hashCode: Int = (running, finished).hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Command_Timings => rep == other.rep
+        case other: Command_Timings => running == other.running && finished == other.finished
         case _ => false
       }
-    override def toString: String = rep.mkString("Command_Timings(", ", ", ")")
+    override def toString: String =
+      running.mkString("Command_Timings(running = (", ", ", "), ") +
+      finished.mkString("finished = (", ", ", "))")
   }
 
 
@@ -96,11 +107,12 @@
         timings = Command_Timings.empty)
 
     def make(
+      now: Time,
       markups: List[Markup] = Nil,
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
-      empty.update(markups = markups, warned = warned, failed = failed)
+      empty.update(now, markups = markups, warned = warned, failed = failed)
     }
 
     def merge(args: IterableOnce[Command_Status]): Command_Status =
@@ -146,6 +158,7 @@
       }
 
     def update(
+      now: Time,
       markups: List[Markup] = Nil,
       warned: Boolean = false,
       failed: Boolean = false
@@ -180,8 +193,10 @@
           case Markup.Command_Timing.name =>
             val props = markup.properties
             val offset = Position.Offset.get(props)
-            val t = Time.seconds(Markup.Elapsed.get(props))
-            timings1 += (offset -> t)
+            val running = props.contains(Markup.command_running)
+            timings1 =
+              if (running) timings1.add_running(offset -> now)
+              else timings1.add_finished(offset -> Time.seconds(Markup.Elapsed.get(props)))
           case _ =>
         }
       }
@@ -231,6 +246,8 @@
       name: Document.Node.Name,
       threshold: Time = Time.max
     ): Node_Status = {
+      val now = Time.now()
+
       val node = version.nodes(name)
 
       var theory_status = Document_Status.Theory_Status.NONE
@@ -259,7 +276,7 @@
         if (status.is_canceled) canceled = true
         if (!status.is_terminated) terminated = false
 
-        val t = status.timings.sum
+        val t = status.timings.sum(now)
         cumulated_time += t
         if (t > max_time) max_time = t
         if (t.is_notable(threshold)) command_timings += (command -> status.timings)
@@ -278,7 +295,7 @@
             }
           case Some(command) =>
             val total = command.span.theory_commands
-            val processed = state.command_status(version, command).timings.count
+            val processed = state.command_status(version, command).timings.count_finished
             percent(processed, total)
         }
       }

--- a/src/Pure/PIDE/markup.ML	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Oct 17 15:13:45 2025 +0200
@@ -223,6 +223,7 @@
   val finalizedN: string val finalized: T
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
+  val command_running: Properties.entry
   val exec_idN: string
   val urgent_properties: Properties.T
   val initN: string
@@ -755,6 +756,8 @@
 val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
+val command_running = (commandN, runningN);
+
 
 (* messages *)
 

--- a/src/Pure/PIDE/markup.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -560,6 +560,8 @@
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
+  val command_running: Properties.Entry = (COMMAND, RUNNING)
+
 
   /* interactive documents */
 

--- a/src/Pure/PIDE/rendering.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -469,6 +469,7 @@
     range: Text.Range,
     focus: Rendering.Focus
   ) : List[Text.Info[Rendering.Color.Value]] = {
+    val now = Time.now()
     for {
       Text.Info(r, result) <-
         snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
@@ -510,7 +511,7 @@
       color <-
         result match {
           case (markups, opt_color) if markups.nonEmpty =>
-            val status = Document_Status.Command_Status.make(markups = markups)
+            val status = Document_Status.Command_Status.make(now, markups = markups)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
             else if (status.is_running) Some(Rendering.Color.running1)
             else if (status.is_canceled) Some(Rendering.Color.canceled)
@@ -668,7 +669,7 @@
             val info2 =
               if (kind == Markup.COMMAND) {
                 val timings = Document_Status.Command_Timings.merge(command_states.map(_.timings))
-                val t = timings(Markup.Command_Offset.get(markup.properties))
+                val t = timings.get_finished(Markup.Command_Offset.get(markup.properties))
                 if (t.is_notable(timing_threshold)) {
                   info1.add_info(r0, Pretty.string(t.message))
                 }
@@ -763,6 +764,7 @@
   /* command status overview */
 
   def overview_color(range: Text.Range): Option[Rendering.Color.Value] = {
+    val now = Time.now()
     if (snapshot.is_outdated) None
     else {
       val results =
@@ -773,7 +775,7 @@
             }, status = true)
       if (results.isEmpty) None
       else {
-        val status = Document_Status.Command_Status.make(markups = results.flatMap(_.info))
+        val status = Document_Status.Command_Status.make(now, markups = results.flatMap(_.info))
 
         if (status.is_running) Some(Rendering.Color.running)
         else if (status.is_failed) Some(Rendering.Color.error)

--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Oct 17 11:03:16 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Oct 17 15:13:45 2025 +0200
@@ -142,13 +142,15 @@
         case Some(doc_view) => doc_view.model.node_name
       }
 
+    val now = Time.now()
+
     val theories =
       List.from(
         for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
           yield Theory_Entry(a, st.cumulated_time.seconds)).sorted(Entry.Ordering)
     val commands =
       (for ((command, timings) <- nodes_status(name).command_timings.toList)
-        yield Command_Entry(command, timings.sum.seconds)).sorted(Entry.Ordering)
+        yield Command_Entry(command, timings.sum(now).seconds)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
       if (entry.name == name) entry.make_current :: commands