# HG changeset patch # User wenzelm # Date 1525706439 -7200 # Node ID 813b5d0904c66ce96cfcb463daa20fc89b85f821 # Parent 0699a0bacc5023c3378015dc4affcfb4e06360ad clarified signature; avoid pointless compression; diff -r 0699a0bacc50 -r 813b5d0904c6 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Mon May 07 17:11:01 2018 +0200 +++ b/src/Pure/Thy/export.ML Mon May 07 17:20:39 2018 +0200 @@ -1,27 +1,27 @@ (* Title: Pure/Thy/export.ML Author: Makarius -Manage theory exports. +Manage theory exports: compressed blobs. *) signature EXPORT = sig - val export: theory -> string -> Output.output -> unit - val export_uncompressed: theory -> string -> Output.output -> unit + val export: theory -> string -> string -> unit + val export_raw: theory -> string -> string list -> unit end; structure Export: EXPORT = struct -fun gen_export compress thy name output = +fun gen_export compress thy name body = (Output.try_protocol_message o Markup.export) {id = Position.get_id (Position.thread_data ()), serial = serial (), theory_name = Context.theory_long_name thy, name = name, - compress = compress} [output]; + compress = compress} body; -val export = gen_export true; -val export_uncompressed = gen_export false; +fun export thy name body = gen_export (size body > 60) thy name [body]; +fun export_raw thy name body = gen_export false thy name body; end; diff -r 0699a0bacc50 -r 813b5d0904c6 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Mon May 07 17:11:01 2018 +0200 +++ b/src/Pure/Thy/export.scala Mon May 07 17:20:39 2018 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/Thy/export.scala Author: Makarius -Manage theory exports. +Manage theory exports: compressed blobs. */ package isabelle