src/Pure/Tools/server_commands.scala
changeset 68167 327bb0f5f768
parent 68152 619de043389f
child 68365 f9379279f98c
equal deleted inserted replaced
68166:021c6fecaf5c 68167:327bb0f5f768
   218                 ("exports" ->
   218                 ("exports" ->
   219                   (if (args.export_pattern == "") Nil else {
   219                   (if (args.export_pattern == "") Nil else {
   220                     val matcher = Export.make_matcher(args.export_pattern)
   220                     val matcher = Export.make_matcher(args.export_pattern)
   221                     for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
   221                     for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
   222                     yield {
   222                     yield {
   223                       val (base64, body) = entry.body.join.maybe_base64
   223                       val (base64, body) = entry.uncompressed().maybe_base64
   224                       JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
   224                       JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
   225                     }
   225                     }
   226                   }))))
   226                   }))))
   227 
   227 
   228       (result_json, result)
   228       (result_json, result)