src/Pure/Tools/build.ML

     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
       |> Real.fmt (StringCvt.FIX (SOME 2));
 
     val timing_props =
       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
-    val _ = Protocol_Message.marker "Timing" timing_props;
+    val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
       else ();

             | NONE => ())
           else ()
         end
       else if function = Markup.theory_timing then
         Protocol_Message.marker (#2 function) args
+      else if function = Markup.session_timing then
+        Protocol_Message.marker "Timing" args
       else
         (case Markup.dest_loading_theory props of
           SOME name => Protocol_Message.marker_text "loading_theory" name
         | NONE => Export.protocol_message props output)
   | [] => raise Output.Protocol_Message props);