src/Pure/Tools/build_job.scala
changeset 72723 3b804e0ffae9
parent 72721 79f5e843e5ec
child 72725 27d9aa2a4010
--- 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")