src/Pure/Thy/export.ML
author wenzelm
Sun May 13 16:26:01 2018 +0200 (13 months ago)
changeset 68167 327bb0f5f768
parent 68146 d23af2dbb4e7
child 69627 3e26471d6d01
permissions -rw-r--r--
clarified implicit compression;
     1 (*  Title:      Pure/Thy/export.ML
     2     Author:     Makarius
     3 
     4 Manage theory exports: compressed blobs.
     5 *)
     6 
     7 signature EXPORT =
     8 sig
     9   val export: theory -> string -> string list -> unit
    10   val export_raw: theory -> string -> string list -> unit
    11 end;
    12 
    13 structure Export: EXPORT =
    14 struct
    15 
    16 fun 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 
    28 fun 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 
    36 val export = gen_export true;
    37 val export_raw = gen_export false;
    38 
    39 end;