diff -r 30767e3da749 -r 61277d1550d6 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Sep 20 22:53:12 2025 +0200 +++ b/src/Pure/PIDE/session.scala Sun Sep 21 13:40:33 2025 +0200 @@ -536,8 +536,7 @@ if (!handled) { msg.properties match { case Protocol.Command_Timing(state_id, props) if prover.defined => - val markup = Markup(Markup.TIMING, props) - val message = XML.elem(Markup.STATUS, List(XML.Elem(markup, Nil))) + val message = XML.elem(Markup.STATUS, List(XML.elem(Markup(Markup.TIMING, props)))) change_command(_.accumulate(state_id, cache.elem(message), cache)) command_timings.post(Session.Command_Timing(props))