src/Pure/Tools/server_commands.scala
changeset 68167 327bb0f5f768
parent 68152 619de043389f
child 68365 f9379279f98c
     1.1 --- a/src/Pure/Tools/server_commands.scala	Sun May 13 16:05:29 2018 +0200
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Sun May 13 16:26:01 2018 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4                      val matcher = Export.make_matcher(args.export_pattern)
     1.5                      for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
     1.6                      yield {
     1.7 -                      val (base64, body) = entry.body.join.maybe_base64
     1.8 +                      val (base64, body) = entry.uncompressed().maybe_base64
     1.9                        JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
    1.10                      }
    1.11                    }))))