more accurate markup for command timing, notably for theory pseudo-command in batch-build, but also for accidental occurrences of command keywords (e.g. in command definition);

--- a/src/Pure/Isar/outer_syntax.ML	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Sep 22 15:55:47 2025 +0200
@@ -289,7 +289,13 @@
     let val name = Token.content_of tok in
       (case lookup_commands thy name of
         NONE => []
-      | SOME cmd => [((Token.pos_of tok, command_markup {def = false} (name, cmd)), "")])
+      | SOME cmd =>
+          let
+            val pos = Token.pos_of tok;
+            val markup =
+              command_markup {def = false} (name, cmd)
+              |> Markup.command_offset (Position.offset_of pos);
+          in [((pos, markup), "")] end)
     end
   else [];
 

--- a/src/Pure/PIDE/markup.ML	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 22 15:55:47 2025 +0200
@@ -206,6 +206,7 @@
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
+  val command_offsetN: string val command_offset: int option -> T -> T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val command_indentN: string val command_indent: int -> T
@@ -716,6 +717,11 @@
 
 (* command timing *)
 
+val command_offsetN = "command_offset";
+fun command_offset offset =
+  let val i = the_default 0 offset
+  in if i = 0 then I else properties [(command_offsetN, Value.print_int i)] end;
+
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>

--- a/src/Pure/PIDE/markup.scala	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Sep 22 15:55:47 2025 +0200
@@ -708,6 +708,7 @@
       }
   }
 
+  val Command_Offset = new Properties.Int("command_offset")
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 

--- a/src/Pure/PIDE/rendering.scala	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Sep 22 15:55:47 2025 +0200
@@ -661,13 +661,14 @@
             for ((i, msg) <- Command.State.get_result_proper(command_states, props))
             yield info.add_message(r0, i, msg)
 
-          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
+          case (info, Text.Info(r0, XML.Elem([e-mail](kind, name), _)))
           if kind != "" && kind != Markup.ML_DEF =>
             val txt = Rendering.gui_name(name, kind = kind)
             val info1 = info.add_info_text(r0, txt, ord = 2)
             val info2 =
               if (kind == Markup.COMMAND) {
-                val t = Document_Status.Command_Timings.merge(command_states.map(_.timings)).sum
+                val timings = Document_Status.Command_Timings.merge(command_states.map(_.timings))
+                val t = timings(Markup.Command_Offset.get(markup.properties))
                 if (t.is_notable(timing_threshold)) {
                   info1.add_info(r0, Pretty.string(t.message))
                 }