more robust: post after state change;
authorwenzelm
Sat, 20 Sep 2025 19:36:59 +0200
changeset 83200 f93e95c4d3cf
parent 83199 8492484a9269
child 83201 d3220d015c9d
more robust: post after state change;
src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Sep 20 18:54:47 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Sep 20 19:36:59 2025 +0200
@@ -536,10 +536,10 @@
           if (!handled) {
             msg.properties match {
               case Protocol.Command_Timing(state_id, props) if prover.defined =>
-                command_timings.post(Session.Command_Timing(props))
                 val markup = Markup(Markup.TIMING, props)
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(markup, Nil)))
                 change_command(_.accumulate(state_id, cache.elem(message), cache))
+                command_timings.post(Session.Command_Timing(props))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))