# HG changeset patch
# User wenzelm
# Date 1607608316 -3600
# Node ID ebf72a3b8daae812897ebc5d359c6436f875e36a
# Parent  612fbd881492dca23548d8ce61a28934816a1ec8
clarified file sources: take from build database instead of file-system;

diff -r 612fbd881492 -r ebf72a3b8daa src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 14:31:34 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 14:51:56 2020 +0100
@@ -30,18 +30,8 @@
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
         val thy_path = Path.explode(thy_file)
-        val thy_source = Symbol.decode(File.read(thy_path))
         val node_name = resources.file_node(thy_path, theory = theory)
 
-        val blobs =
-          blobs_files.map(file =>
-          {
-            val path = Path.explode(file)
-            val src_path = File.relative_path(thy_path, path).getOrElse(path)
-            Command.Blob.read_file(resources.file_node(path), src_path)
-          })
-        val blobs_info = Command.Blobs_Info(blobs.map(Exn.Res(_)))
-
         val results =
           Command.Results.make(
             for {
@@ -49,10 +39,30 @@
               i <- Markup.Serial.unapply(markup.properties)
             } yield i -> tree)
 
-        val thy_xml = read_xml(Export.MARKUP)
+        val blobs =
+          blobs_files.map(file =>
+          {
+            val path = Path.explode(file)
+            val name = resources.file_node(path)
+            val src_path = File.relative_path(thy_path, path).getOrElse(path)
+            Command.Blob(name, src_path, None)
+          })
         val blobs_xml =
           for (i <- (1 to blobs.length).toList)
-          yield read_xml(Export.MARKUP + i)
+            yield read_xml(Export.MARKUP + i)
+
+        val blobs_info =
+          Command.Blobs_Info(
+            for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
+              yield {
+                val text = XML.content(xml)
+                val chunk = Symbol.Text_Chunk(text)
+                val digest = SHA1.digest(Symbol.encode(text))
+                Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
+              })
+
+        val thy_xml = read_xml(Export.MARKUP)
+        val thy_source = XML.content(thy_xml)
 
         val markups_index =
           Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)