src/Pure/Build/build.scala
changeset 82951 c5b07e7ab7f3
parent 82950 a4e457dc735e
child 82972 ae65438eec0c
equal deleted inserted replaced
82950:a4e457dc735e 82951:c5b07e7ab7f3
   727     yield {
   727     yield {
   728       val thy_file = migrate_file(thy_file0)
   728       val thy_file = migrate_file(thy_file0)
   729 
   729 
   730       val blobs =
   730       val blobs =
   731         blobs_files0.map { case (command_offset, name0) =>
   731         blobs_files0.map { case (command_offset, name0) =>
   732           val name = migrate_file(name0)
   732           val node_name = Document.Node.Name(migrate_file(name0))
       
   733           val src_path = Path.explode(name0)
   733 
   734 
   734           val file = read_source_file(name0)
   735           val file = read_source_file(name0)
   735           val bytes = file.bytes
   736           val bytes = file.bytes
   736           val text = decode(bytes.text)
   737           val text = decode(bytes.text)
   737           val chunk = Symbol.Text_Chunk(text)
   738           val chunk = Symbol.Text_Chunk(text)
   738           val content = Some((file.digest, chunk))
   739           val content = Some((file.digest, chunk))
   739 
   740 
   740           Command.Blob(command_offset, Document.Node.Name(name), Path.explode(name0), content) ->
   741           Command.Blob(command_offset, node_name, src_path, content) ->
   741             Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
   742             Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
   742         }
   743         }
   743 
   744 
   744       val thy_source = decode(read_source_file(thy_file0).bytes.text)
   745       val thy_source = decode(read_source_file(thy_file0).bytes.text)
   745       val thy_xml = read_xml(Export.MARKUP)
   746       val thy_xml = read_xml(Export.MARKUP)