# HG changeset patch
# User wenzelm
# Date 1585822749 -7200
# Node ID dad29591645a47c3d62a7b852a85aa12ca797b4b
# Parent  0aef1812ae3a51d0db12672dd1c7abb33123e802
proper arguments of protocol function;

diff -r 0aef1812ae3a -r dad29591645a src/Pure/PIDE/session.scala
--- 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 =>