--- 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(markup@Markup.Entity(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))
}