src/Pure/Tools/server_commands.scala
changeset 76852 2915740fce1f
parent 76656 a8f452f7c503
child 77137 79231a210f5d
equal deleted inserted replaced
76851:69f6895dd7d4 76852:2915740fce1f
   264                 ("exports" ->
   264                 ("exports" ->
   265                   (if (args.export_pattern == "") Nil else {
   265                   (if (args.export_pattern == "") Nil else {
   266                     val matcher = Export.make_matcher(List(args.export_pattern))
   266                     val matcher = Export.make_matcher(List(args.export_pattern))
   267                     for { entry <- snapshot.exports if matcher(entry.entry_name) }
   267                     for { entry <- snapshot.exports if matcher(entry.entry_name) }
   268                     yield {
   268                     yield {
   269                       val (base64, body) = entry.uncompressed.maybe_encode_base64
   269                       val (base64, body) = entry.bytes.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