author | wenzelm |
Sat, 02 Feb 2019 15:52:14 +0100 | |
changeset 69784 | 24bbc4e30e5b |
parent 69650 | c95edf19133b |
child 69788 | c175499a7537 |
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 |
|
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
9 |
val export: theory -> Path.T -> string list -> unit |
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
10 |
val export_raw: theory -> Path.T -> string list -> unit |
69650 | 11 |
val markup: theory -> string -> Markup.T |
12 |
val message: theory -> string -> string |
|
68090 | 13 |
end; |
14 |
||
15 |
structure Export: EXPORT = |
|
16 |
struct |
|
17 |
||
69648 | 18 |
(* export *) |
19 |
||
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
20 |
fun check_name path = |
68105 | 21 |
let |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
22 |
val name = Path.implode path; |
69627 | 23 |
val _ = |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
24 |
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
|
25 |
else error ("Bad export name: " ^ quote name); |
68105 | 26 |
in name end; |
27 |
||
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
28 |
fun gen_export compress thy path body = |
68090 | 29 |
(Output.try_protocol_message o Markup.export) |
30 |
{id = Position.get_id (Position.thread_data ()), |
|
68101 | 31 |
serial = serial (), |
68090 | 32 |
theory_name = Context.theory_long_name thy, |
69784
24bbc4e30e5b
clarified signature: Path.T as in Generated_Files;
wenzelm
parents:
69650
diff
changeset
|
33 |
name = check_name path, |
68146 | 34 |
compress = compress} body; |
68090 | 35 |
|
68167 | 36 |
val export = gen_export true; |
68113 | 37 |
val export_raw = gen_export false; |
68090 | 38 |
|
69648 | 39 |
|
40 |
(* information message *) |
|
41 |
||
69650 | 42 |
fun markup thy s = |
43 |
let val name = (Markup.nameN, Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s)) |
|
44 |
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; |
|
69648 | 45 |
|
69650 | 46 |
fun message thy s = |
47 |
"See " ^ Markup.markup (markup thy s) "theory exports"; |
|
69648 | 48 |
|
68090 | 49 |
end; |