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