13 object Build_Job |
13 object Build_Job |
14 { |
14 { |
15 /* theory markup/messages from database */ |
15 /* theory markup/messages from database */ |
16 |
16 |
17 def read_theory( |
17 def read_theory( |
18 db_context: Sessions.Database_Context, session: String, theory: String): Option[Command] = |
18 db_context: Sessions.Database_Context, |
|
19 resources: Resources, |
|
20 session: String, |
|
21 theory: String): Option[Command] = |
19 { |
22 { |
20 def read(name: String): Export.Entry = |
23 def read(name: String): Export.Entry = |
21 db_context.get_export(List(session), theory, name) |
24 db_context.get_export(List(session), theory, name) |
22 |
25 |
23 def read_xml(name: String): XML.Body = |
26 def read_xml(name: String): XML.Body = |
24 db_context.xml_cache.body( |
27 db_context.xml_cache.body( |
25 YXML.parse_body(Symbol.decode(UTF8.decode_permissive(read(name).uncompressed)))) |
28 YXML.parse_body(Symbol.decode(UTF8.decode_permissive(read(name).uncompressed)))) |
26 |
29 |
27 (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { |
30 (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { |
28 case (Value.Long(id), thy_file :: blobs_files) => |
31 case (Value.Long(id), thy_file :: blobs_files) => |
29 val node_name = Document.Node.Name(thy_file, Thy_Header.dir_name(thy_file), theory) |
|
30 val thy_path = Path.explode(thy_file) |
32 val thy_path = Path.explode(thy_file) |
31 val thy_source = Symbol.decode(File.read(thy_path)) |
33 val thy_source = Symbol.decode(File.read(thy_path)) |
|
34 val node_name = resources.file_node(thy_path, theory = theory) |
32 |
35 |
33 val blobs = |
36 val blobs = |
34 blobs_files.map(file => |
37 blobs_files.map(file => |
35 { |
38 { |
36 val master_dir = Thy_Header.dir_name(file) |
|
37 val path = Path.explode(file) |
39 val path = Path.explode(file) |
38 val src_path = File.relative_path(thy_path, path).getOrElse(path) |
40 val src_path = File.relative_path(thy_path, path).getOrElse(path) |
39 Command.Blob.read_file(Document.Node.Name(file, master_dir), src_path) |
41 Command.Blob.read_file(resources.file_node(path), src_path) |
40 }) |
42 }) |
41 val blobs_info = Command.Blobs_Info(blobs.map(Exn.Res(_))) |
43 val blobs_info = Command.Blobs_Info(blobs.map(Exn.Res(_))) |
42 |
44 |
43 val results = |
45 val results = |
44 Command.Results.make( |
46 Command.Results.make( |