src/Pure/Build/export.ML

clarified signature: separate formal context from exported theory_name;

(*  Title:      Pure/Build/export.ML
    Author:     Makarius

Manage per-session theory exports: compressed blobs.
*)

signature EXPORT =
sig
  val report: Context.generic -> string -> Path.binding -> unit
  type params =
    {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool}
  val export_params: Context.generic -> params -> XML.body -> unit
  val export: theory -> Path.binding -> XML.body -> unit
  val export_executable: theory -> Path.binding -> XML.body -> unit
  val export_file: theory -> Path.binding -> Path.T -> unit
  val export_executable_file: theory -> Path.binding -> Path.T -> unit
  val markup: theory -> Path.T -> Markup.T
  val message: theory -> Path.T -> string
end;

structure Export: EXPORT =
struct

(* export *)

fun report context theory_name binding =
  let
    val (path, pos) = Path.dest_binding binding;
    val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
  in Context_Position.report_generic context pos markup end;

type params =
  {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool};

fun export_params context ({theory_name, binding, executable, compress, strict}: params) body =
 (report context theory_name binding;
  (Output.try_protocol_message o Markup.export)
   {id = Position.id_of (Position.thread_data ()),
    serial = serial (),
    theory_name = theory_name,
    name = Path.implode_binding (tap Path.proper_binding binding),
    executable = executable,
    compress = compress,
    strict = strict} [body]);

fun export thy binding body =
  export_params (Context.Theory thy)
    {theory_name = Context.theory_long_name thy, binding = binding,
      executable = false, compress = true, strict = true} body;

fun export_executable thy binding body =
  export_params (Context.Theory thy)
    {theory_name = Context.theory_long_name thy, binding = binding,
      executable = true, compress = true, strict = true} body;

fun export_file thy binding file =
  export thy binding (Bytes.contents_blob (Bytes.read file));

fun export_executable_file thy binding file =
  export_executable thy binding (Bytes.contents_blob (Bytes.read file));


(* information message *)

fun markup thy path =
  let
    val thy_path = Path.basic (Context.theory_long_name thy) + path;
    val name = (Markup.nameN, Path.implode thy_path);
  in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;

fun message thy path =
  "See " ^ Markup.markup (markup thy path) "theory exports";

end;