equal
deleted
inserted
replaced
264 ("exports" -> |
264 ("exports" -> |
265 (if (args.export_pattern == "") Nil else { |
265 (if (args.export_pattern == "") Nil else { |
266 val matcher = Export.make_matcher(args.export_pattern) |
266 val matcher = Export.make_matcher(args.export_pattern) |
267 for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } |
267 for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } |
268 yield { |
268 yield { |
269 val (base64, body) = entry.uncompressed.maybe_base64 |
269 val (base64, body) = entry.uncompressed.maybe_encode_base64 |
270 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) |
270 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) |
271 } |
271 } |
272 })) |
272 })) |
273 })) |
273 })) |
274 |
274 |