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) |