author | wenzelm |
Sat, 30 Mar 2019 22:51:38 +0100 | |
changeset 70016 | a8142ac5e4b6 |
parent 70015 | c8e08d8ffb93 |
child 70051 | 7a4dc1e60dc8 |
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 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
9 |
type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool} |
69788 | 10 |
val export_params: params -> string list -> unit |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
11 |
val export: theory -> Path.binding -> string list -> unit |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
12 |
val export_executable: theory -> Path.binding -> string list -> unit |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
13 |
val export_file: theory -> Path.binding -> Path.T -> unit |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
14 |
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
|
15 |
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
|
16 |
val message: theory -> Path.T -> string |
68090 | 17 |
end; |
18 |
||
19 |
structure Export: EXPORT = |
|
20 |
struct |
|
21 |
||
69648 | 22 |
(* export *) |
23 |
||
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
24 |
type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}; |
68105 | 25 |
|
70016 | 26 |
fun export_params ({theory = thy, binding, executable, compress}: params) blob = |
27 |
let |
|
28 |
val theory_name = Context.theory_long_name thy; |
|
29 |
val name = Path.implode_binding binding; |
|
30 |
val (path, pos) = Path.dest_binding binding; |
|
31 |
val _ = |
|
32 |
Context_Position.report_generic (Context.Theory thy) pos |
|
33 |
(Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path))); |
|
34 |
in |
|
35 |
(Output.try_protocol_message o Markup.export) |
|
36 |
{id = Position.get_id (Position.thread_data ()), |
|
37 |
serial = serial (), |
|
38 |
theory_name = theory_name, |
|
39 |
name = name, |
|
40 |
executable = executable, |
|
41 |
compress = compress} blob |
|
42 |
end; |
|
68090 | 43 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
44 |
fun export thy binding blob = |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
45 |
export_params {theory = thy, binding = binding, executable = false, compress = true} blob; |
69788 | 46 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
47 |
fun export_executable thy binding blob = |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
48 |
export_params {theory = thy, binding = binding, executable = true, compress = true} blob; |
70013 | 49 |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
50 |
fun export_file thy binding file = export thy binding [File.read file]; |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
51 |
fun export_executable_file thy binding file = export_executable thy binding [File.read file]; |
68090 | 52 |
|
69648 | 53 |
|
54 |
(* information message *) |
|
55 |
||
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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
val name = (Markup.nameN, Path.implode thy_path); |
69650 | 60 |
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; |
69648 | 61 |
|
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
|
62 |
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
|
63 |
"See " ^ Markup.markup (markup thy path) "theory exports"; |
69648 | 64 |
|
68090 | 65 |
end; |