--- a/src/Pure/Tools/build_job.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Nov 23 15:14:58 2020 +0100
@@ -120,9 +120,9 @@
private def loading_theory(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
- case Markup.Loading_Theory(name) =>
+ case Markup.Loading_Theory(Markup.Name(name)) =>
progress.theory(Progress.Theory(name, session = session_name))
- true
+ false
case _ => false
}
@@ -158,6 +158,18 @@
case Session.Runtime_Statistics(props) => runtime_statistics += props
}
+ session.finished_theories += Session.Consumer[Command.State]("finished_theories")
+ {
+ case st =>
+ val command = st.command
+ val theory_name = command.node_name.theory
+ val args = Protocol.Export.Args(theory_name = theory_name, name = Export.MARKUP)
+ val xml =
+ st.markups(Command.Markup_Index.markup)
+ .to_XML(command.range, command.source, Markup.Elements.full)
+ export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
+ }
+
session.all_messages += Session.Consumer[Any]("build_session_output")
{
case msg: Prover.Output =>