1(*  Title:      Pure/Thy/export.ML
2    Author:     Makarius
3
4Manage theory exports: compressed blobs.
5*)
6
7signature EXPORT =
8sig
9  val export: theory -> string -> string list -> unit
10  val export_raw: theory -> string -> string list -> unit
11end;
12
13structure Export: EXPORT =
14struct
15
16fun check_name name =
17  let
18    fun err () = error ("Bad export name " ^ quote name);
19    fun check_elem elem =
20      if member (op =) ["", ".", ".."] elem then err ()
21      else ignore (Path.basic elem handle ERROR _ => err ());
22
23    val elems = space_explode "/" name;
24    val _ = null elems andalso err ();
25    val _ = List.app check_elem elems;
26  in name end;
27
28fun gen_export compress thy name body =
29  (Output.try_protocol_message o Markup.export)
30   {id = Position.get_id (Position.thread_data ()),
31    serial = serial (),
32    theory_name = Context.theory_long_name thy,
33    name = check_name name,
34    compress = compress} body;
35
36val export = gen_export true;
37val export_raw = gen_export false;
38
39end;
40