src/Pure/Tools/generated_files.ML
author wenzelm
Tue, 28 Sep 2021 16:01:13 +0200
changeset 74373 6e4093927dbb
parent 74147 d030b988d470
child 74561 8e6c973003c8
permissions -rw-r--r--
outer syntax: support for control-cartouche tokens;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69383
747f8b052e59 clarified modules;
wenzelm
parents: 69381
diff changeset
     1
(*  Title:      Pure/Tools/generated_files.ML
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
     3
69383
747f8b052e59 clarified modules;
wenzelm
parents: 69381
diff changeset
     4
Generated source files for other languages: with antiquotations, without Isabelle symbols.
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
     5
*)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
     6
69383
747f8b052e59 clarified modules;
wenzelm
parents: 69381
diff changeset
     7
signature GENERATED_FILES =
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
     8
sig
70015
c8e08d8ffb93 clarified signature: more explicit type Path.binding;
wenzelm
parents: 70013
diff changeset
     9
  val add_files: Path.binding * string -> theory -> theory
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    10
  type file = {path: Path.T, pos: Position.T, content: string}
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    11
  val file_binding: file -> Path.binding
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    12
  val file_markup: file -> Markup.T
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    13
  val print_file: file -> string
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    14
  val report_file: Proof.context -> Position.T -> file -> unit
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    15
  val get_files: theory -> file list
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    16
  val get_file: theory -> Path.binding -> file
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    17
  val get_files_in: Path.binding list * theory -> (file * Position.T) list
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    18
  val check_files_in: Proof.context ->
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    19
    (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    20
  val write_file: Path.T -> file -> unit
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    21
  val export_file: theory -> file -> unit
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    22
  type file_type =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    23
    {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    24
  val file_type:
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    25
    binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    26
    theory -> theory
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    27
  val antiquotation: binding -> 'a Token.context_parser ->
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    28
    ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    29
    theory -> theory
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    30
  val set_string: string -> Proof.context -> Proof.context
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    31
  val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    32
  val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    33
  val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    34
  val export_generated_files_cmd: Proof.context ->
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
    35
    ((string * Position.T) list * (string * Position.T) option) list -> unit
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    36
  val with_compile_dir: (Path.T -> unit) -> unit
70054
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    37
  val compile_generated_files: Proof.context ->
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    38
    (Path.binding list * theory) list ->
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    39
    (Path.T list * Path.T) list ->
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    40
    (Path.binding list * bool option) list ->
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    41
    Path.binding -> Input.source -> unit
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    42
  val compile_generated_files_cmd: Proof.context ->
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    43
    ((string * Position.T) list * (string * Position.T) option) list ->
72841
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
    44
    (Input.source list * Input.source) list ->
70054
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
    45
    ((string * Position.T) list * bool option) list ->
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
    46
    string * Position.T -> Input.source -> unit
70067
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
    47
  val execute: Path.T -> Input.source -> string -> string
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    48
end;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    49
69383
747f8b052e59 clarified modules;
wenzelm
parents: 69381
diff changeset
    50
structure Generated_Files: GENERATED_FILES =
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    51
struct
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    52
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    53
(** context data **)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    54
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    55
type file = Path.T * (Position.T * string);
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    56
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    57
type file_type =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    58
  {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    59
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    60
type antiquotation = Token.src -> Proof.context -> file_type -> string;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    61
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    62
fun err_dup_files path pos pos' =
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    63
  error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']);
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    64
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    65
structure Data = Theory_Data
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    66
(
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    67
  type T =
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    68
    file list Symtab.table *  (*files for named theory*)
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    69
    file_type Name_Space.table *  (*file types*)
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
    70
    antiquotation Name_Space.table;  (*antiquotations*)
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    71
  val empty =
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    72
    (Symtab.empty,
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
    73
     Name_Space.empty_table Markup.file_typeN,
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
    74
     Name_Space.empty_table Markup.antiquotationN);
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    75
  val extend = I;
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    76
  fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    77
    let
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    78
      val files' =
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    79
        (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) =>
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    80
          if path1 <> path2 then false
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    81
          else if file1 = file2 then true
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    82
          else err_dup_files path1 (#1 file1) (#1 file2))));
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    83
      val types' = Name_Space.merge_tables (types1, types2);
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    84
      val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
    85
    in (files', types', antiqs') end;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    86
);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
    87
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    88
fun lookup_files thy =
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    89
  Symtab.lookup_list (#1 (Data.get thy)) (Context.theory_long_name thy);
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    90
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    91
fun update_files thy_files' thy =
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    92
  (Data.map o @{apply 3(1)}) (Symtab.update (Context.theory_long_name thy, thy_files')) thy;
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    93
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    94
fun add_files (binding, content) thy =
70055
36fb663145e5 type Path.binding may be empty: check later via proper_binding;
wenzelm
parents: 70054
diff changeset
    95
  let
36fb663145e5 type Path.binding may be empty: check later via proper_binding;
wenzelm
parents: 70054
diff changeset
    96
    val _ = Path.proper_binding binding;
36fb663145e5 type Path.binding may be empty: check later via proper_binding;
wenzelm
parents: 70054
diff changeset
    97
    val (path, pos) = Path.dest_binding binding;
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    98
    val thy_files = lookup_files thy;
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
    99
    val thy_files' =
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
   100
      (case AList.lookup (op =) thy_files path of
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
   101
        SOME (pos', _) => err_dup_files path pos pos'
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
   102
      | NONE => (path, (pos, content)) :: thy_files);
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
   103
  in update_files thy_files' thy end;
72046
c386d1b77762 more thorough extend/merge (for Theory.join_theory);
wenzelm
parents: 70991
diff changeset
   104
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   105
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   106
(* get files *)
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   107
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   108
type file = {path: Path.T, pos: Position.T, content: string};
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   109
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   110
fun file_binding (file: file) = Path.binding (#path file, #pos file);
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   111
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   112
fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   113
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   114
fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file)));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   115
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   116
fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file);
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   117
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   118
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   119
fun get_files thy =
72050
d4de7e4754d2 clarified theory data: more robust merge;
wenzelm
parents: 72046
diff changeset
   120
  lookup_files thy |> rev |> map (fn (path, (pos, content)) =>
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   121
    {path = path, pos = pos, content = content}: file);
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   122
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   123
fun get_file thy binding =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   124
  let val (path, pos) = Path.dest_binding binding in
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   125
    (case find_first (fn file => #path file = path) (get_files thy) of
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   126
      SOME file => file
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   127
    | NONE =>
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   128
        error ("Missing generated file " ^ Path.print path ^
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   129
          " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   130
  end;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   131
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   132
fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   133
  | get_files_in (files, thy) =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   134
      map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files;
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   135
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   136
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   137
(* check and output files *)
69628
a2fbfdc5e62d export generated files;
wenzelm
parents: 69385
diff changeset
   138
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   139
fun check_files_in ctxt (files, opt_thy) =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   140
  let
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   141
    val thy =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   142
      (case opt_thy of
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   143
        SOME name => Theory.check {long = false} ctxt name
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   144
      | NONE => Proof_Context.theory_of ctxt);
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   145
  in (map Path.explode_binding files, thy) end;
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   146
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   147
fun write_file dir (file: file) =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   148
  let
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72375
diff changeset
   149
    val path = Path.expand (dir + #path file);
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 72050
diff changeset
   150
    val _ = Isabelle_System.make_directory (Path.dir path);
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   151
    val _ = File.generate path (#content file);
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   152
  in () end;
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   153
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   154
fun export_file thy (file: file) =
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70067
diff changeset
   155
  Export.export thy (file_binding file) [XML.Text (#content file)];
70013
6de8b7a5cd44 tuned signature -- more operations;
wenzelm
parents: 70012
diff changeset
   156
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   157
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   158
(* file types *)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   159
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   160
fun get_file_type thy ext =
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   161
  if ext = "" then error "Bad file extension"
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   162
  else
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   163
    (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   164
      (fn (_, file_type) => fn res =>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   165
        if #ext file_type = ext then SOME file_type else res)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   166
    |> (fn SOME file_type => file_type
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   167
         | NONE => error ("Unknown file type for extension " ^ quote ext));
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   168
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   169
fun file_type binding {ext, make_comment, make_string} thy =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   170
  let
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   171
    val name = Binding.name_of binding;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   172
    val pos = Binding.pos_of binding;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   173
    val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   174
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   175
    val table = #2 (Data.get thy);
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   176
    val space = Name_Space.space_of_table table;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   177
    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   178
    val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   179
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   180
    val _ =
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   181
      (case try (#name o get_file_type thy) ext of
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   182
        NONE => ()
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   183
      | SOME name' =>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   184
          error ("Extension " ^ quote ext ^ " already registered for file type " ^
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   185
            quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   186
  in thy |> (Data.map o @{apply 3(2)}) (K data') end;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   187
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   188
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   189
(* antiquotations *)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   190
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   191
val get_antiquotations = #3 o Data.get o Proof_Context.theory_of;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   192
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   193
fun antiquotation name scan body thy =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   194
  let
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   195
    fun ant src ctxt file_type : string =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   196
      let val (x, ctxt') = Token.syntax scan src ctxt
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   197
      in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   198
  in
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   199
    thy
69385
be9f187dcd50 clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents: 69383
diff changeset
   200
    |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   201
  end;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   202
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   203
val scan_antiq =
74373
6e4093927dbb outer syntax: support for control-cartouche tokens;
wenzelm
parents: 74147
diff changeset
   204
  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   205
  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   206
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   207
fun read_source ctxt (file_type: file_type) source =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   208
  let
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   209
    val _ =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   210
      Context_Position.report ctxt (Input.pos_of source)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   211
        (Markup.language
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   212
          {name = #name file_type, symbols = false, antiquotes = true,
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   213
            delimited = Input.is_delimited source});
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   214
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   215
    val (input, _) =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   216
      Input.source_explode source
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   217
      |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   218
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   219
    val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   220
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   221
    fun expand antiq =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   222
      (case antiq of
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   223
        Antiquote.Text s => s
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   224
      | Antiquote.Control {name, body, ...} =>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   225
          let
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   226
            val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   227
            val (src', ant) = Token.check_src ctxt get_antiquotations src;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   228
          in ant src' ctxt file_type end
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   229
      | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   230
  in implode (map expand input) end;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   231
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   232
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   233
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   234
(** Isar commands **)
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   235
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   236
(* generate_file *)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   237
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   238
fun generate_file (binding, source) lthy =
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   239
  let
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   240
    val thy = Proof_Context.theory_of lthy;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   241
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   242
    val (path, pos) = Path.dest_binding binding;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   243
    val file_type =
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   244
      get_file_type thy (#2 (Path.split_ext path))
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   245
        handle ERROR msg => error (msg ^ Position.here pos);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   246
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   247
    val header = #make_comment file_type " generated by Isabelle ";
70012
36aeb535a801 tuned signature;
wenzelm
parents: 69784
diff changeset
   248
    val content = header ^ "\n" ^ read_source lthy file_type source;
70015
c8e08d8ffb93 clarified signature: more explicit type Path.binding;
wenzelm
parents: 70013
diff changeset
   249
  in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   250
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   251
fun generate_file_cmd (file, source) lthy =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   252
  generate_file (Path.explode_binding file, source) lthy;
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   253
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   254
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   255
(* export_generated_files *)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   256
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   257
fun export_generated_files ctxt args =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   258
  let val thy = Proof_Context.theory_of ctxt in
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   259
    (case map #1 (maps get_files_in args) of
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   260
      [] => ()
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   261
    | files =>
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   262
       (List.app (export_file thy) files;
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   263
        writeln (Export.message thy Path.current);
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   264
        writeln (cat_lines (map (prefix "  " o print_file) files))))
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   265
  end;
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   266
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   267
fun export_generated_files_cmd ctxt args =
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   268
  export_generated_files ctxt (map (check_files_in ctxt) args);
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   269
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   270
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   271
(* compile_generated_files *)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   272
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   273
val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   274
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   275
fun with_compile_dir body : unit =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   276
  body (Path.explode (Config.get (Context.the_local_context ()) compile_dir));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   277
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   278
fun compile_generated_files ctxt args external export export_prefix source =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   279
  Isabelle_System.with_tmp_dir "compile" (fn dir =>
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   280
    let
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   281
      val thy = Proof_Context.theory_of ctxt;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   282
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   283
      val files = maps get_files_in args;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   284
      val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   285
      val _ = List.app (write_file dir o #1) files;
70054
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   286
      val _ =
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   287
        external |> List.app (fn (files, base_dir) =>
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   288
          files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   289
      val _ =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   290
        ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   291
          ML_Compiler.flags (Input.pos_of source)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   292
          (ML_Lex.read "Generated_Files.with_compile_dir (" @
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   293
            ML_Lex.read_source source @ ML_Lex.read ")");
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   294
      val _ =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   295
        export |> List.app (fn (bindings, executable) =>
70053
997f256c98e3 proper .exe path for export;
wenzelm
parents: 70051
diff changeset
   296
          bindings |> List.app (fn binding0 =>
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   297
            let
70053
997f256c98e3 proper .exe path for export;
wenzelm
parents: 70051
diff changeset
   298
              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
997f256c98e3 proper .exe path for export;
wenzelm
parents: 70051
diff changeset
   299
              val (path, pos) = Path.dest_binding binding;
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   300
              val content =
72511
460d743010bc clarified signature: overloaded "+" for Path.append;
wenzelm
parents: 72375
diff changeset
   301
                (case try File.read (dir + path) of
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   302
                  SOME context => context
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   303
                | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   304
              val _ = Export.report_export thy export_prefix;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   305
              val binding' =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   306
                Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   307
            in
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   308
              (if is_some executable then Export.export_executable else Export.export)
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 70067
diff changeset
   309
                thy binding' [XML.Text content]
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   310
            end));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   311
      val _ =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   312
        if null export then ()
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   313
        else writeln (Export.message thy (Path.path_of_binding export_prefix));
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   314
    in () end);
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   315
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   316
fun compile_generated_files_cmd ctxt args external export export_prefix source =
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   317
  compile_generated_files ctxt
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   318
    (map (check_files_in ctxt) args)
70054
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   319
    (external |> map (fn (raw_files, raw_base_dir) =>
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   320
      let
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   321
        val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
72841
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
   322
        fun check source =
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
   323
         (Resources.check_file ctxt (SOME base_dir) source;
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
   324
          Path.explode (Input.string_of source));
70054
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   325
        val files = map check raw_files;
a884b2967dd7 clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents: 70053
diff changeset
   326
      in (files, base_dir) end))
70051
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   327
    ((map o apfst o map) Path.explode_binding export)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   328
    (Path.explode_binding export_prefix)
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   329
    source;
7a4dc1e60dc8 added command 'compile_generated_files';
wenzelm
parents: 70049
diff changeset
   330
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   331
70067
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   332
(* execute compiler -- auxiliary *)
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   333
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   334
fun execute dir title compile =
74147
d030b988d470 provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents: 74142
diff changeset
   335
  Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir)
73279
37aff2142295 clarified signature;
wenzelm
parents: 72841
diff changeset
   336
  |> Process_Result.check
37aff2142295 clarified signature;
wenzelm
parents: 72841
diff changeset
   337
  |> Process_Result.out
70067
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   338
    handle ERROR msg =>
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   339
      let val (s, pos) = Input.source_content title
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   340
      in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   341
9b34dbeb1103 auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents: 70055
diff changeset
   342
70047
96fe857a7a6f clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents: 70015
diff changeset
   343
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   344
(** concrete file types **)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   345
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   346
val _ =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   347
  Theory.setup
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   348
    (file_type \<^binding>\<open>Haskell\<close>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   349
      {ext = "hs",
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   350
       make_comment = enclose "{-" "-}",
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   351
       make_string = GHC.print_string});
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   352
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   353
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   354
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   355
(** concrete antiquotations **)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   356
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   357
(* ML expression as string literal *)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   358
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   359
structure Local_Data = Proof_Data
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   360
(
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   361
  type T = string option;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   362
  fun init _ = NONE;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   363
);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   364
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   365
val set_string = Local_Data.put o SOME;
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   366
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   367
fun the_string ctxt =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   368
  (case Local_Data.get ctxt of
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   369
    SOME s => s
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   370
  | NONE => raise Fail "No result string");
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   371
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   372
val _ =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   373
  Theory.setup
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   374
    (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   375
      (fn {context = ctxt, file_type, argument, ...} =>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   376
        ctxt |> Context.proof_map
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   377
          (ML_Context.expression (Input.pos_of argument)
69383
747f8b052e59 clarified modules;
wenzelm
parents: 69381
diff changeset
   378
            (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   379
             ML_Lex.read_source argument @ ML_Lex.read "))"))
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   380
        |> the_string |> #make_string file_type));
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   382
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   383
(* file-system paths *)
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   384
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   385
fun path_antiquotation binding check =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   386
  antiquotation binding
72841
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
   387
    (Args.context -- Scan.lift Parse.path_input >>
fd8d82c4433b more accurate markup (refining 1c59b555ac4a);
wenzelm
parents: 72511
diff changeset
   388
      (fn (ctxt, source) => (check ctxt (SOME Path.current) source |> Path.implode)))
69381
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   389
    (fn {file_type, argument, ...} => #make_string file_type argument);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   390
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   391
val _ =
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   392
  Theory.setup
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   393
   (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   394
    path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   395
    path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   396
4c9b4e2c5460 more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff changeset
   397
end;