equal
deleted
inserted
replaced
1 (* Title: Pure/Thy/export.ML |
1 (* Title: Pure/Thy/export.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Manage theory exports. |
4 Manage theory exports: compressed blobs. |
5 *) |
5 *) |
6 |
6 |
7 signature EXPORT = |
7 signature EXPORT = |
8 sig |
8 sig |
9 val export: theory -> string -> Output.output -> unit |
9 val export: theory -> string -> string -> unit |
10 val export_uncompressed: theory -> string -> Output.output -> unit |
10 val export_raw: theory -> string -> string list -> unit |
11 end; |
11 end; |
12 |
12 |
13 structure Export: EXPORT = |
13 structure Export: EXPORT = |
14 struct |
14 struct |
15 |
15 |
16 fun gen_export compress thy name output = |
16 fun gen_export compress thy name body = |
17 (Output.try_protocol_message o Markup.export) |
17 (Output.try_protocol_message o Markup.export) |
18 {id = Position.get_id (Position.thread_data ()), |
18 {id = Position.get_id (Position.thread_data ()), |
19 serial = serial (), |
19 serial = serial (), |
20 theory_name = Context.theory_long_name thy, |
20 theory_name = Context.theory_long_name thy, |
21 name = name, |
21 name = name, |
22 compress = compress} [output]; |
22 compress = compress} body; |
23 |
23 |
24 val export = gen_export true; |
24 fun export thy name body = gen_export (size body > 60) thy name [body]; |
25 val export_uncompressed = gen_export false; |
25 fun export_raw thy name body = gen_export false thy name body; |
26 |
26 |
27 end; |
27 end; |