--- a/src/Pure/PIDE/session.scala Wed Apr 01 23:04:28 2020 +0200
+++ b/src/Pure/PIDE/session.scala Thu Apr 02 12:19:09 2020 +0200
@@ -486,12 +486,12 @@
init_protocol_handler(name)
case Protocol.Command_Timing(state_id, timing) if prover.defined =>
- command_timings.post(Session.Command_Timing(msg.properties))
+ command_timings.post(Session.Command_Timing(msg.properties.tail))
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
case Protocol.Theory_Timing(_, _) =>
- theory_timings.post(Session.Theory_Timing(msg.properties))
+ theory_timings.post(Session.Theory_Timing(msg.properties.tail))
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>