# HG changeset patch # User wenzelm # Date 1554381058 -7200 # Node ID 7a4dc1e60dc8a87d7ac9fce0eb232695ec688216 # Parent 5b66e6672ccf92f88fe3a58d79e772c508867dc6 added command 'compile_generated_files'; tuned signature; diff -r 5b66e6672ccf -r 7a4dc1e60dc8 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Apr 04 14:29:49 2019 +0200 +++ b/src/Pure/Pure.thy Thu Apr 04 14:30:58 2019 +0200 @@ -23,6 +23,7 @@ and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag + and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix" and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" @@ -126,6 +127,7 @@ (Parse.path_binding -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) >> Generated_Files.generate_file_cmd); + val files_in = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\in\ |-- Parse.!!! Parse.theory_name); @@ -137,6 +139,28 @@ Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))) + + val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false; + + val executable = + \<^keyword>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; + + val export_files = Scan.repeat1 Parse.path_binding -- executable; + + val _ = + Outer_Syntax.command \<^command_keyword>\compile_generated_files\ + "compile generated files and export results" + (Parse.and_list files_in -- + Scan.optional (\<^keyword>\external_files\ |-- + Parse.!!! (Scan.repeat1 (Parse.position Parse.path))) [] -- + Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- + Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("compiled", Position.none) -- + (Parse.where_ |-- Parse.!!! Parse.ML_source) + >> (fn ((((args, external), export), export_prefix), source) => + Toplevel.keep (fn st => + Generated_Files.compile_generated_files_cmd + (Toplevel.context_of st) args external export export_prefix source))); + in end\ diff -r 5b66e6672ccf -r 7a4dc1e60dc8 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Thu Apr 04 14:29:49 2019 +0200 +++ b/src/Pure/Thy/export.ML Thu Apr 04 14:30:58 2019 +0200 @@ -6,6 +6,7 @@ signature EXPORT = sig + val report_export: theory -> Path.binding -> unit type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool} val export_params: params -> string list -> unit val export: theory -> Path.binding -> string list -> unit @@ -21,25 +22,24 @@ (* export *) +fun report_export thy binding = + let + val theory_name = Context.theory_long_name thy; + val (path, pos) = Path.dest_binding binding; + val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)); + in Context_Position.report_generic (Context.Theory thy) pos markup end; + type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}; fun export_params ({theory = thy, binding, executable, compress}: params) blob = - let - val theory_name = Context.theory_long_name thy; - val name = Path.implode_binding binding; - val (path, pos) = Path.dest_binding binding; - val _ = - Context_Position.report_generic (Context.Theory thy) pos - (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path))); - in - (Output.try_protocol_message o Markup.export) - {id = Position.get_id (Position.thread_data ()), - serial = serial (), - theory_name = theory_name, - name = name, - executable = executable, - compress = compress} blob - end; + (report_export thy binding; + (Output.try_protocol_message o Markup.export) + {id = Position.get_id (Position.thread_data ()), + serial = serial (), + theory_name = Context.theory_long_name thy, + name = Path.implode_binding binding, + executable = executable, + compress = compress} blob); fun export thy binding blob = export_params {theory = thy, binding = binding, executable = false, compress = true} blob; diff -r 5b66e6672ccf -r 7a4dc1e60dc8 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Thu Apr 04 14:29:49 2019 +0200 +++ b/src/Pure/Tools/generated_files.ML Thu Apr 04 14:30:58 2019 +0200 @@ -9,10 +9,12 @@ val add_files: Path.binding * string -> theory -> theory type file = {path: Path.T, pos: Position.T, content: string} val file_binding: file -> Path.binding + val file_markup: file -> Markup.T val print_file: file -> string + val report_file: Proof.context -> Position.T -> file -> unit val get_files: theory -> file list val get_file: theory -> Path.binding -> file - val get_files_in: Path.binding list * theory -> file list + val get_files_in: Path.binding list * theory -> (file * Position.T) 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 @@ -31,6 +33,13 @@ 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 + val with_compile_dir: (Path.T -> unit) -> unit + val compile_generated_files: Proof.context -> (Path.binding list * theory) list -> + Path.T list -> (Path.binding list * bool option) list -> Path.binding -> Input.source -> unit + val compile_generated_files_cmd: Proof.context -> + ((string * Position.T) list * (string * Position.T) option) list -> + (string * Position.T) list -> ((string * Position.T) list * bool option) list -> + string * Position.T -> Input.source -> unit end; structure Generated_Files: GENERATED_FILES = @@ -76,9 +85,12 @@ 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 file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file)); + +fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file))); + +fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file); + fun get_files thy = Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) => @@ -93,8 +105,9 @@ " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos)) end; -fun get_files_in ([], thy) = get_files thy - | get_files_in (files, thy) = map (get_file thy) files; +fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy) + | get_files_in (files, thy) = + map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files; (* check and output files *) @@ -196,6 +209,8 @@ (** Isar commands **) +(* generate_file *) + fun generate_file (binding, source) lthy = let val thy = Proof_Context.theory_of lthy; @@ -212,9 +227,12 @@ fun generate_file_cmd (file, source) lthy = generate_file (Path.explode_binding file, source) lthy; + +(* export_generated_files *) + fun export_generated_files ctxt args = let val thy = Proof_Context.theory_of ctxt in - (case maps get_files_in args of + (case map #1 (maps get_files_in args) of [] => () | files => (List.app (export_file thy) files; @@ -224,7 +242,58 @@ fun export_generated_files_cmd ctxt args = export_generated_files ctxt (map (check_files_in ctxt) args); - + + +(* compile_generated_files *) + +val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K ""); + +fun with_compile_dir body : unit = + body (Path.explode (Config.get (Context.the_local_context ()) compile_dir)); + +fun compile_generated_files ctxt args external export export_prefix source = + Isabelle_System.with_tmp_dir "compile" (fn dir => + let + val thy = Proof_Context.theory_of ctxt; + + val files = maps get_files_in args; + val _ = List.app (fn (file, pos) => report_file ctxt pos file) files; + val _ = List.app (write_file dir o #1) files; + val _ = external |> List.app (fn file => Isabelle_System.copy_file file dir); + val _ = + ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt)) + ML_Compiler.flags (Input.pos_of source) + (ML_Lex.read "Generated_Files.with_compile_dir (" @ + ML_Lex.read_source source @ ML_Lex.read ")"); + val _ = + export |> List.app (fn (bindings, executable) => + bindings |> List.app (fn binding => + let + val (path, pos) = Path.dest_binding binding |>> executable = SOME true ? Path.exe; + val content = + (case try File.read (Path.append dir path) of + SOME context => context + | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos)); + val _ = Export.report_export thy export_prefix; + val binding' = + Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding; + in + (if is_some executable then Export.export_executable else Export.export) + thy binding' [content] + end)); + val _ = + if null export then () + else writeln (Export.message thy (Path.path_of_binding export_prefix)); + in () end); + +fun compile_generated_files_cmd ctxt args external export export_prefix source = + compile_generated_files ctxt + (map (check_files_in ctxt) args) + (map (Resources.check_file ctxt NONE) external) + ((map o apfst o map) Path.explode_binding export) + (Path.explode_binding export_prefix) + source; + (** concrete file types **)