--- a/src/Pure/Tools/build_job.scala Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Nov 26 16:08:39 2020 +0100
@@ -166,7 +166,7 @@
val args = Protocol.Export.Args(theory_name = theory_name, name = name)
export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
}
- export(Export.MARKUP, snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
+ export(Export.MARKUP, snapshot.xml_markup())
}
session.all_messages += Session.Consumer[Any]("build_session_output")