src/Pure/Tools/server_commands.scala
changeset 75587 79b4efd17d2b
parent 75394 42267c650205
child 75658 5905c7f484b3
equal deleted inserted replaced
75586:b2b097624e4c 75587:79b4efd17d2b
   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