# HG changeset patch
# User wenzelm
# Date 1672918985 -3600
# Node ID 80ff0ce76b5e851fb6033d7f6ed847a5ed64e3e4
# Parent  c27fcf4a74955f5bcd36f95897d735ab5fc4f3a8
tuned;

diff -r c27fcf4a7495 -r 80ff0ce76b5e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Jan 04 16:40:02 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Jan 05 12:43:05 2023 +0100
@@ -30,11 +30,6 @@
       (thy_file, blobs_files) <- theory_context.files(permissive = true)
     }
     yield {
-      val results =
-        Command.Results.make(
-          for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
-            yield i -> elem)
-
       val master_dir =
         Path.explode(Url.strip_base_name(thy_file).getOrElse(
           error("Cannot determine theory master directory: " + quote(thy_file))))
@@ -70,10 +65,15 @@
           for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
           yield index -> Markup_Tree.from_XML(xml))
 
+      val results =
+        Command.Results.make(
+          for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
+            yield i -> elem)
+
       val command =
         Command.unparsed(thy_source, theory = true, id = id,
           node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
-          blobs_info = blobs_info, results = results, markups = markups)
+          blobs_info = blobs_info, markups = markups, results = results)
 
       Document.State.init.snippet(command)
     }