src/Pure/Thy/export.ML
author wenzelm
Mon, 07 May 2018 18:25:26 +0200
changeset 68105 577072a0ceed
parent 68102 813b5d0904c6
child 68113 c925f53fd1f6
permissions -rw-r--r--
more checks;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/export.ML
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     3
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
     4
Manage theory exports: compressed blobs.
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     5
*)
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     6
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     7
signature EXPORT =
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
     8
sig
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
     9
  val export: theory -> string -> string -> unit
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
    10
  val export_raw: theory -> string -> string list -> unit
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    11
end;
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    12
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    13
structure Export: EXPORT =
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    14
struct
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    15
68105
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    16
fun check_name name =
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    17
  let
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    18
    fun err () = error ("Bad export name " ^ quote name);
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    19
    fun check_elem elem =
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    20
      if member (op =) ["", ".", ".."] elem then err ()
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    21
      else ignore (Path.basic elem handle ERROR _ => err ());
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    22
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    23
    val elems = space_explode "/" name;
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    24
    val _ = null elems andalso err ();
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    25
    val _ = List.app check_elem elems;
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    26
  in name end;
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    27
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
    28
fun gen_export compress thy name body =
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    29
  (Output.try_protocol_message o Markup.export)
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    30
   {id = Position.get_id (Position.thread_data ()),
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68090
diff changeset
    31
    serial = serial (),
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    32
    theory_name = Context.theory_long_name thy,
68105
577072a0ceed more checks;
wenzelm
parents: 68102
diff changeset
    33
    name = check_name name,
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
    34
    compress = compress} body;
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    35
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
    36
fun export thy name body = gen_export (size body > 60) thy name [body];
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
    37
fun export_raw thy name body = gen_export false thy name body;
68090
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    38
7c8ed28dd40a tuned signature;
wenzelm
parents:
diff changeset
    39
end;