tuned;
authorwenzelm
Thu, 05 Jan 2023 12:43:05 +0100
changeset 76911 80ff0ce76b5e
parent 76910 c27fcf4a7495
child 76912 ca872f20cf5b
tuned;
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)
     }