# HG changeset patch
# User wenzelm
# Date 1606392957 -3600
# Node ID 4fa1aa5dac4f80f3383d09efd23856c03e8555ea
# Parent  7cef6b1a6682e9cd2760df043fa6a3f8c0f5716d
tuned;

diff -r 7cef6b1a6682 -r 4fa1aa5dac4f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 12:27:09 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 13:15:57 2020 +0100
@@ -161,12 +161,17 @@
         {
           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)))
+            val markup = st.markups(Command.Markup_Index.markup)
+
+            def export(name: String, xml: XML.Body)
+            {
+              val theory_name = command.node_name.theory
+              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,
+              markup.to_XML(command.range, command.source, Markup.Elements.full))
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")