equal
deleted
inserted
replaced
33 val thy_path = Path.explode(thy_file) |
33 val thy_path = Path.explode(thy_file) |
34 val node_name = resources.file_node(thy_path, theory = theory) |
34 val node_name = resources.file_node(thy_path, theory = theory) |
35 |
35 |
36 val results = |
36 val results = |
37 Command.Results.make( |
37 Command.Results.make( |
38 for { |
38 for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) |
39 elem @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES) |
39 yield i -> elem) |
40 i <- Markup.Serial.unapply(markup.properties) |
|
41 } yield i -> elem) |
|
42 |
40 |
43 val blobs = |
41 val blobs = |
44 blobs_files.map(file => |
42 blobs_files.map(file => |
45 { |
43 { |
46 val path = Path.explode(file) |
44 val path = Path.explode(file) |