# HG changeset patch # User wenzelm # Date 1554321000 -7200 # Node ID 96fe857a7a6f598dde6a14ba27fc1cb19930327a # Parent c37525278ae2ab61cd7093eb58927098410e06de clarified signature: more explicit operations for corresponding Isar commands; diff -r c37525278ae2 -r 96fe857a7a6f src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Wed Apr 03 21:11:21 2019 +0200 +++ b/src/Pure/Isar/parse.ML Wed Apr 03 21:50:00 2019 +0200 @@ -70,6 +70,7 @@ val embedded_position: (string * Position.T) parser val text: string parser val path: string parser + val path_binding: (string * Position.T) parser val session_name: (string * Position.T) parser val theory_name: (string * Position.T) parser val liberal_name: string parser @@ -282,6 +283,7 @@ val text = group (fn () => "text") (embedded || verbatim); val path = group (fn () => "file name/path specification") embedded; +val path_binding = group (fn () => "path binding (strict file name)") (position embedded); val session_name = group (fn () => "session name") name_position; val theory_name = group (fn () => "theory name") name_position; diff -r c37525278ae2 -r 96fe857a7a6f src/Pure/Pure.thy --- a/src/Pure/Pure.thy Wed Apr 03 21:11:21 2019 +0200 +++ b/src/Pure/Pure.thy Wed Apr 03 21:50:00 2019 +0200 @@ -123,29 +123,20 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" - (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) + (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); + val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ - "export generated files from this or other theories" - (Scan.repeat Parse.name_position >> (fn names => + "export generated files from given theories" + (Parse.and_list1 files_in >> (fn args => Toplevel.keep (fn st => - let - val ctxt = Toplevel.context_of st; - val thy = Toplevel.theory_of st; - val other_thys = - if null names then [thy] - else map (Theory.check {long = false} ctxt) names; - val paths = Generated_Files.export_files thy other_thys; - in - if not (null paths) then - (writeln (Export.message thy Path.current); - writeln (cat_lines (paths |> map (fn (path, pos) => - Markup.markup (Markup.entityN, Position.def_properties_of pos) - (quote (Path.implode path)))))) - else () - end))); + Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))) + in end\ diff -r c37525278ae2 -r 96fe857a7a6f src/Pure/Tools/generated_files.ML --- 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 _ = diff -r c37525278ae2 -r 96fe857a7a6f src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Wed Apr 03 21:11:21 2019 +0200 +++ b/src/Tools/Haskell/Haskell.thy Wed Apr 03 21:50:00 2019 +0200 @@ -1943,6 +1943,6 @@ return () \ -export_generated_files +export_generated_files _ end diff -r c37525278ae2 -r 96fe857a7a6f src/Tools/Haskell/Test.thy --- a/src/Tools/Haskell/Test.thy Wed Apr 03 21:11:21 2019 +0200 +++ b/src/Tools/Haskell/Test.thy Wed Apr 03 21:50:00 2019 +0200 @@ -11,10 +11,11 @@ Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir => let val src_dir = Path.append tmp_dir (Path.explode "src"); - val files = Generated_Files.write_files \<^theory>\Haskell\ src_dir; + val files = Generated_Files.get_files \<^theory>\Haskell\; + val _ = List.app (Generated_Files.write_file src_dir) files; val modules = files - |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode "."); + |> map (#path #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode "."); val _ = GHC.new_project tmp_dir {name = "isabelle",