equal
deleted
inserted
replaced
23 { |
23 { |
24 def read(name: String): Export.Entry = |
24 def read(name: String): Export.Entry = |
25 db_context.get_export(List(session), theory, name) |
25 db_context.get_export(List(session), theory, name) |
26 |
26 |
27 def read_xml(name: String): XML.Body = |
27 def read_xml(name: String): XML.Body = |
28 db_context.cache.body(YXML.parse_body( |
28 YXML.parse_body( |
29 Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)))) |
29 Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), |
|
30 cache = db_context.cache) |
30 |
31 |
31 (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { |
32 (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { |
32 case (Value.Long(id), thy_file :: blobs_files) => |
33 case (Value.Long(id), thy_file :: blobs_files) => |
33 val node_name = resources.file_node(Path.explode(thy_file), theory = theory) |
34 val node_name = resources.file_node(Path.explode(thy_file), theory = theory) |
34 |
35 |