--- a/src/Pure/Tools/generated_files.ML Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML Wed Apr 03 21:50:00 2019 +0200
@@ -7,10 +7,16 @@
signature GENERATED_FILES =
sig
val add_files: Path.binding * string -> theory -> theory
- val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
- val write_files: theory -> Path.T -> (Path.T * Position.T) list
- val export_files: theory -> theory list -> (Path.T * Position.T) list
- val the_file_content: theory -> Path.T -> string
+ type file = {path: Path.T, pos: Position.T, content: string}
+ val file_binding: file -> Path.binding
+ val print_file: file -> string
+ val get_files: theory -> file list
+ val get_file: theory -> Path.binding -> file
+ val get_files_in: Path.binding list * theory -> file list
+ val check_files_in: Proof.context ->
+ (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
+ val write_file: Path.T -> file -> unit
+ val export_file: theory -> file -> unit
type file_type =
{name: string, ext: string, make_comment: string -> string, make_string: string -> string}
val file_type:
@@ -20,7 +26,11 @@
({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
theory -> theory
val set_string: string -> Proof.context -> Proof.context
+ val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
+ val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
+ val export_generated_files_cmd: Proof.context ->
+ ((string * Position.T) list * (string * Position.T) option) list -> unit
end;
structure Generated_Files: GENERATED_FILES =
@@ -50,9 +60,6 @@
Name_Space.merge_tables (antiqs1, antiqs2));
);
-
-(* files *)
-
fun add_files (binding, content) =
let val (path, pos) = Path.dest_binding binding in
(Data.map o @{apply 3(1)}) (fn files =>
@@ -62,34 +69,58 @@
| NONE => (path, (pos, content)) :: files))
end;
-val get_files =
- map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}) o
- rev o #1 o Data.get;
+
+(* get files *)
+
+type file = {path: Path.T, pos: Position.T, content: string};
+
+fun file_binding (file: file) = Path.binding (#path file, #pos file);
+
+fun print_file (file: file) =
+ quote (Path.implode (#path file))
+ |> Markup.markup (Markup.entityN, Position.def_properties_of (#pos file));
-fun write_files thy dir =
- get_files thy |> map (fn {path, pos, content} =>
- let
- val path' = Path.expand (Path.append dir path);
- val _ = Isabelle_System.mkdirs (Path.dir path');
- val _ = File.generate path' content;
- in (path, pos) end);
+fun get_files thy =
+ Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
+ {path = path, pos = pos, content = content}: file);
+
+fun get_file thy binding =
+ let val (path, pos) = Path.dest_binding binding in
+ (case find_first (fn file => #path file = path) (get_files thy) of
+ SOME file => file
+ | NONE =>
+ error ("Missing generated file " ^ Path.print path ^
+ " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
+ end;
-fun export_files thy other_thys =
- other_thys |> maps (fn other_thy =>
- get_files other_thy |> map (fn {path, pos, content} =>
- (Export.export thy (Path.binding (path, pos)) [content]; (path, pos))));
+fun get_files_in ([], thy) = get_files thy
+ | get_files_in (files, thy) = map (get_file thy) files;
+
+
+(* check and output files *)
-fun the_file_content thy path =
- (case find_first (fn file => #path file = path) (get_files thy) of
- SOME {content, ...} => content
- | NONE =>
- error ("Missing generated file " ^ Path.print path ^
- " in theory " ^ quote (Context.theory_long_name thy)));
+fun check_files_in ctxt (files, opt_thy) =
+ let
+ val thy =
+ (case opt_thy of
+ SOME name => Theory.check {long = false} ctxt name
+ | NONE => Proof_Context.theory_of ctxt);
+ in (map Path.explode_binding files, thy) end;
+
+fun write_file dir (file: file) =
+ let
+ val path = Path.expand (Path.append dir (#path file));
+ val _ = Isabelle_System.mkdirs (Path.dir path);
+ val _ = File.generate path (#content file);
+ in () end;
+
+fun export_file thy (file: file) =
+ Export.export thy (file_binding file) [#content file];
(* file types *)
-fun the_file_type thy ext =
+fun get_file_type thy ext =
if ext = "" then error "Bad file extension"
else
(#2 (Data.get thy), NONE) |-> Name_Space.fold_table
@@ -110,7 +141,7 @@
val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
val _ =
- (case try (#name o the_file_type thy) ext of
+ (case try (#name o get_file_type thy) ext of
NONE => ()
| SOME name' =>
error ("Extension " ^ quote ext ^ " already registered for file type " ^
@@ -162,24 +193,40 @@
in implode (map expand input) end;
-(* generate files *)
-fun generate_file_cmd ((file, pos), source) lthy =
+(** Isar commands **)
+
+fun generate_file (binding, source) lthy =
let
val thy = Proof_Context.theory_of lthy;
- val path = Path.explode file;
- val binding = Path.binding (path, pos);
+ val (path, pos) = Path.dest_binding binding;
val file_type =
- the_file_type thy (#2 (Path.split_ext path))
+ get_file_type thy (#2 (Path.split_ext path))
handle ERROR msg => error (msg ^ Position.here pos);
val header = #make_comment file_type " generated by Isabelle ";
val content = header ^ "\n" ^ read_source lthy file_type source;
in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
+fun generate_file_cmd (file, source) lthy =
+ generate_file (Path.explode_binding file, source) lthy;
+
+fun export_generated_files ctxt args =
+ let val thy = Proof_Context.theory_of ctxt in
+ (case maps get_files_in args of
+ [] => ()
+ | files =>
+ (List.app (export_file thy) files;
+ writeln (Export.message thy Path.current);
+ writeln (cat_lines (map (prefix " " o print_file) files))))
+ end;
+
+fun export_generated_files_cmd ctxt args =
+ export_generated_files ctxt (map (check_files_in ctxt) args);
+
(** concrete file types **)
val _ =