author | wenzelm |
Sun, 29 Mar 2020 13:25:59 +0200 | |
changeset 71619 | e33f6e5f86b6 |
parent 70991 | f9f7c34b7dd4 |
child 71622 | ab5009192ebb |
permissions | -rw-r--r-- |
68090 | 1 |
(* Title: Pure/Thy/export.ML |
2 |
Author: Makarius |
|
3 |
||
68102 | 4 |
Manage theory exports: compressed blobs. |
68090 | 5 |
*) |
6 |
||
7 |
signature EXPORT = |
|
8 |
sig |
|
70051 | 9 |
val report_export: theory -> Path.binding -> unit |
70499 | 10 |
type params = |
11 |
{theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool} |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
12 |
val export_params: params -> XML.body -> unit |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
13 |
val export: theory -> Path.binding -> XML.body -> unit |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
14 |
val export_executable: theory -> Path.binding -> XML.body -> unit |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
15 |
val export_file: theory -> Path.binding -> Path.T -> unit |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
16 |
val export_executable_file: theory -> Path.binding -> Path.T -> unit |
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
17 |
val markup: theory -> Path.T -> Markup.T |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
18 |
val message: theory -> Path.T -> string |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
19 |
val protocol_message: Output.protocol_message_fn |
68090 | 20 |
end; |
21 |
||
22 |
structure Export: EXPORT = |
|
23 |
struct |
|
24 |
||
69648 | 25 |
(* export *) |
26 |
||
70051 | 27 |
fun report_export thy binding = |
28 |
let |
|
29 |
val theory_name = Context.theory_long_name thy; |
|
30 |
val (path, pos) = Path.dest_binding binding; |
|
31 |
val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)); |
|
32 |
in Context_Position.report_generic (Context.Theory thy) pos markup end; |
|
33 |
||
70499 | 34 |
type params = |
35 |
{theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}; |
|
68105 | 36 |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
37 |
fun export_params ({theory = thy, binding, executable, compress, strict}: params) body = |
70051 | 38 |
(report_export thy binding; |
39 |
(Output.try_protocol_message o Markup.export) |
|
40 |
{id = Position.get_id (Position.thread_data ()), |
|
41 |
serial = serial (), |
|
42 |
theory_name = Context.theory_long_name thy, |
|
70055
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70051
diff
changeset
|
43 |
name = Path.implode_binding (tap Path.proper_binding binding), |
70051 | 44 |
executable = executable, |
70499 | 45 |
compress = compress, |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
46 |
strict = strict} body); |
68090 | 47 |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
48 |
fun export thy binding body = |
70499 | 49 |
export_params |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
50 |
{theory = thy, binding = binding, executable = false, compress = true, strict = true} body; |
69788 | 51 |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
52 |
fun export_executable thy binding body = |
70499 | 53 |
export_params |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
54 |
{theory = thy, binding = binding, executable = true, compress = true, strict = true} body; |
70013 | 55 |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
56 |
fun export_file thy binding file = |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
57 |
export thy binding [XML.Text (File.read file)]; |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
58 |
|
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
59 |
fun export_executable_file thy binding file = |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
60 |
export_executable thy binding [XML.Text (File.read file)]; |
68090 | 61 |
|
69648 | 62 |
|
63 |
(* information message *) |
|
64 |
||
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
65 |
fun markup thy path = |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
66 |
let |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
67 |
val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path; |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
68 |
val name = (Markup.nameN, Path.implode thy_path); |
69650 | 69 |
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; |
69648 | 70 |
|
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
71 |
fun message thy path = |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69788
diff
changeset
|
72 |
"See " ^ Markup.markup (markup thy path) "theory exports"; |
69648 | 73 |
|
70907 | 74 |
|
75 |
(* protocol message (bootstrap) *) |
|
76 |
||
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
77 |
fun protocol_message props body = |
70907 | 78 |
(case props of |
79 |
function :: args => |
|
80 |
if function = (Markup.functionN, Markup.exportN) andalso |
|
81 |
not (null args) andalso #1 (hd args) = Markup.idN |
|
82 |
then |
|
83 |
let |
|
84 |
val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ())); |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
85 |
val _ = YXML.write_body path body; |
71619
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70991
diff
changeset
|
86 |
in |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70991
diff
changeset
|
87 |
Protocol_Message.inline_properties (#2 function) |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70991
diff
changeset
|
88 |
(tl args @ [(Markup.fileN, Path.implode path)]) |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70991
diff
changeset
|
89 |
end |
70907 | 90 |
else raise Output.Protocol_Message props |
91 |
| [] => raise Output.Protocol_Message props); |
|
92 |
||
93 |
val _ = |
|
94 |
if Thread_Data.is_virtual then () |
|
95 |
else Private_Output.protocol_message_fn := protocol_message; |
|
96 |
||
68090 | 97 |
end; |