equal
deleted
inserted
replaced
218 ("exports" -> |
218 ("exports" -> |
219 (if (args.export_pattern == "") Nil else { |
219 (if (args.export_pattern == "") Nil else { |
220 val matcher = Export.make_matcher(args.export_pattern) |
220 val matcher = Export.make_matcher(args.export_pattern) |
221 for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) } |
221 for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) } |
222 yield { |
222 yield { |
223 val (base64, body) = entry.body.join.maybe_base64 |
223 val (base64, body) = entry.uncompressed().maybe_base64 |
224 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) |
224 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) |
225 } |
225 } |
226 })))) |
226 })))) |
227 |
227 |
228 (result_json, result) |
228 (result_json, result) |