equal
deleted
inserted
replaced
261 (for { |
261 (for { |
262 (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) |
262 (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) |
263 } yield output_message(tree, pos))) + |
263 } yield output_message(tree, pos))) + |
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(List(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_encode_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 } |