src/Pure/PIDE/session.scala
changeset 83203 61277d1550d6
parent 83200 f93e95c4d3cf
child 83209 a39fde2f020a
--- 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))