equal
deleted
inserted
replaced
534 case msg: Prover.Protocol_Output => |
534 case msg: Prover.Protocol_Output => |
535 val handled = protocol_handlers.invoke(msg) |
535 val handled = protocol_handlers.invoke(msg) |
536 if (!handled) { |
536 if (!handled) { |
537 msg.properties match { |
537 msg.properties match { |
538 case Protocol.Command_Timing(state_id, props) if prover.defined => |
538 case Protocol.Command_Timing(state_id, props) if prover.defined => |
539 val markup = Markup(Markup.TIMING, props) |
539 val message = XML.elem(Markup.STATUS, List(XML.elem(Markup(Markup.TIMING, props)))) |
540 val message = XML.elem(Markup.STATUS, List(XML.Elem(markup, Nil))) |
|
541 change_command(_.accumulate(state_id, cache.elem(message), cache)) |
540 change_command(_.accumulate(state_id, cache.elem(message), cache)) |
542 command_timings.post(Session.Command_Timing(props)) |
541 command_timings.post(Session.Command_Timing(props)) |
543 |
542 |
544 case Markup.Theory_Timing(props) => |
543 case Markup.Theory_Timing(props) => |
545 theory_timings.post(Session.Theory_Timing(props)) |
544 theory_timings.post(Session.Theory_Timing(props)) |