src/Pure/Tools/server_commands.scala
changeset 75658 5905c7f484b3
parent 75587 79b4efd17d2b
child 75674 c8e6078fee73
equal deleted inserted replaced
75657:900b76040211 75658:5905c7f484b3
   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                     }