author | wenzelm |
Fri, 29 Mar 2019 13:42:17 +0100 | |
changeset 70011 | 9dde788b0128 |
parent 70009 | 435fb018e8ee |
child 70013 | 6de8b7a5cd44 |
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 |
|
70011 | 9 |
val check_name: Path.T -> string |
69788 | 10 |
type params = {theory: theory, path: Path.T, executable: bool, compress: bool} |
11 |
val export_params: params -> string list -> unit |
|
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
12 |
val export: theory -> Path.T -> string list -> unit |
69788 | 13 |
val export_executable: theory -> Path.T -> string list -> 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
|
14 |
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
|
15 |
val message: theory -> Path.T -> string |
68090 | 16 |
end; |
17 |
||
18 |
structure Export: EXPORT = |
|
19 |
struct |
|
20 |
||
69648 | 21 |
(* export *) |
22 |
||
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
23 |
fun check_name path = |
68105 | 24 |
let |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
25 |
val name = Path.implode path; |
69627 | 26 |
val _ = |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
27 |
if not (Path.is_current path) andalso Path.all_basic path then () |
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
28 |
else error ("Bad export name: " ^ quote name); |
68105 | 29 |
in name end; |
30 |
||
69788 | 31 |
type params = {theory: theory, path: Path.T, executable: bool, compress: bool}; |
32 |
||
33 |
fun export_params ({theory, path, executable, compress}: params) blob = |
|
68090 | 34 |
(Output.try_protocol_message o Markup.export) |
35 |
{id = Position.get_id (Position.thread_data ()), |
|
68101 | 36 |
serial = serial (), |
69788 | 37 |
theory_name = Context.theory_long_name theory, |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
38 |
name = check_name path, |
69788 | 39 |
executable = executable, |
40 |
compress = compress} blob; |
|
68090 | 41 |
|
69788 | 42 |
fun export theory path blob = |
43 |
export_params {theory = theory, path = path, executable = false, compress = true} blob; |
|
44 |
||
45 |
fun export_executable theory path blob = |
|
46 |
export_params {theory = theory, path = path, executable = true, compress = true} blob; |
|
68090 | 47 |
|
69648 | 48 |
|
49 |
(* information message *) |
|
50 |
||
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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
val name = (Markup.nameN, Path.implode thy_path); |
69650 | 55 |
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; |
69648 | 56 |
|
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
|
57 |
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
|
58 |
"See " ^ Markup.markup (markup thy path) "theory exports"; |
69648 | 59 |
|
68090 | 60 |
end; |