# HG changeset patch
# User wenzelm
# Date 1607607094 -3600
# Node ID 612fbd881492dca23548d8ce61a28934816a1ec8
# Parent  a261946dafa3d500e7a303ec6add528c9a51f11d
tuned;

diff -r a261946dafa3 -r 612fbd881492 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 14:13:03 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 14:31:34 2020 +0100
@@ -49,15 +49,17 @@
               i <- Markup.Serial.unapply(markup.properties)
             } yield i -> tree)
 
-        val markup_index_blobs =
+        val thy_xml = read_xml(Export.MARKUP)
+        val blobs_xml =
+          for (i <- (1 to blobs.length).toList)
+          yield read_xml(Export.MARKUP + i)
+
+        val markups_index =
           Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
         val markups =
           Command.Markups.make(
-            for ((index, i) <- markup_index_blobs.zipWithIndex)
-            yield {
-              val xml = read_xml(Export.MARKUP + (if (i == 0) "" else i.toString))
-              index -> Markup_Tree.from_XML(xml)
-            })
+            for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
+            yield index -> Markup_Tree.from_XML(xml))
 
         val command =
           Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,