# HG changeset patch # User wenzelm # Date 1554409269 -7200 # Node ID 06edf32c60573451722256e5aca0933bebb280b6 # Parent 7b6add80e3a575310c354874aceca6b1a886b801# Parent 43acf9a457f0be44dfd9c9a2319821ade44d3e74 merged diff -r 7b6add80e3a5 -r 06edf32c6057 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Apr 04 16:38:45 2019 +0100 +++ b/Admin/components/components.sha1 Thu Apr 04 22:21:09 2019 +0200 @@ -254,6 +254,7 @@ b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz 27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz +4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz diff -r 7b6add80e3a5 -r 06edf32c6057 Admin/components/main --- a/Admin/components/main Thu Apr 04 16:38:45 2019 +0100 +++ b/Admin/components/main Thu Apr 04 22:21:09 2019 +0200 @@ -17,7 +17,7 @@ scala-2.12.8 smbc-0.4.1 spass-3.8ds-1 -sqlite-jdbc-3.23.1 +sqlite-jdbc-3.27.2.1 ssh-java-20190323 stack-1.9.3 vampire-4.2.2 diff -r 7b6add80e3a5 -r 06edf32c6057 NEWS --- a/NEWS Thu Apr 04 16:38:45 2019 +0100 +++ b/NEWS Thu Apr 04 22:21:09 2019 +0200 @@ -41,6 +41,13 @@ need to provide a closed expression -- without trailing semicolon. Minor INCOMPATIBILITY. +* Commands 'generate_file', 'export_generated_files', and +'compile_generated_files' support a stateless (PIDE-conformant) model +for generated sources and compiled binaries of other languages. The +compilation processed is managed in Isabelle/ML, and results exported to +the session database for further use (e.g. with "isabelle export" or +"isabelle build -e"). + *** Isabelle/jEdit Prover IDE *** diff -r 7b6add80e3a5 -r 06edf32c6057 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Thu Apr 04 22:21:09 2019 +0200 @@ -665,7 +665,7 @@ ; definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \ - @{syntax mixfix}? @'=' @{syntax term} + @'and'); + @{syntax mixfix}? '=' @{syntax term} + @'and'); \ The core of each interpretation command is a locale expression \expr\; the @@ -1188,22 +1188,105 @@ \ -section \External file dependencies\ +section \Generated files and external files\ text \ - \begin{matharray}{rcl} + Write access to the physical file-system is incompatible with the stateless + model of processing Isabelle documents. To avoid bad effects, the theory + context maintains a logical ``file-system'' for generated files, as a + mapping of structured file-names to content. Names need to be unique for + each theory node. When exporting generated files for other purposes, the + (long) theory name is prefixed for extra qualification, but there are also + means to smash overlong paths. See also @{cite "isabelle-system"} for + \<^theory_text>\export_files\ within session \<^verbatim>\ROOT\ files, together with @{tool build} + option \<^verbatim>\-e\. + + \begin{matharray}{rcll} + @{command_def "generate_file"} & : & \local_theory \ local_theory\ \\ + @{command_def "export_generated_files"} & : & \context \\ \\ + @{command_def "compile_generated_files"} & : & \context \\ \\ @{command_def "external_file"} & : & \any \ any\ \\ \end{matharray} - \<^rail>\@@{command external_file} @{syntax name} ';'?\ + \<^rail>\ + @@{command generate_file} path '=' content + ; + path: @{syntax embedded} + ; + content: @{syntax embedded} + ; + @@{command export_generated_files} (files_in_theory + @'and') + ; + files_in_theory: (@'_' | (path+)) (('(' @'in' @{syntax name} ')')?) + ; + @@{command compile_generated_files} (files_in_theory + @'and') \ + (@'external_files' (external_files + @'and'))? \ + (@'export_files' (export_files + @'and'))? \ + (@'export_prefix' path)? + ; + external_files: (path+) (('(' @'in' path ')')?) + ; + export_files: (path+) (executable?) + ; + executable: '(' ('exe' | 'executable') ')' + ; + @@{command external_file} @{syntax name} ';'? + \ + + \<^descr> \<^theory_text>\generate_file path = content\ augments the table of generated files + within the current theory by a new entry: duplicates are not allowed. The + name extension determines a pre-existent file-type; the \content\ is a + string that is preprocessed according to rules of this file-type. + + For example, Isabelle/Pure supports \<^verbatim>\.hs\ as file-type for Haskell: + embedded cartouches are evaluated as Isabelle/ML expressions of type + \<^ML_type>\string\, the result is inlined in Haskell string syntax. + + \<^descr> \<^theory_text>\export_generated_files paths (in thy)\ retrieves named generated files + from the given theory (that needs be reachable via imports of the current + one). By default, the current theory node is used. Using ``\<^verbatim>\_\'' + (underscore) instead of explicit path names refers to \emph{all} files of a + theory node. + + The overall list of files is prefixed with the respective (long) theory name + and exported to the session database. In Isabelle/jEdit the result can be + browsed via the virtual file-system with prefix ``\<^verbatim>\isabelle-export:\'' + (using the regular file-browser). + + \<^descr> \<^theory_text>\compile_generated_files paths (in thy) where compile_body\ retrieves + named generated files as for \<^theory_text>\export_generated_files\ and writes them into + a temporary directory, such that the \compile_body\ may operate on them as + an ML function of type \<^ML_type>\Path.T -> unit\. This may create further + files, e.g.\ executables produced by a compiler that is invoked as external + process (e.g.\ via \<^ML>\Isabelle_System.bash\), or any other files. + + The option ``\<^theory_text>\external_files paths (in base_dir)\'' copies files from the + physical file-system into the temporary directory, \emph{before} invoking + \compile_body\. The \base_dir\ prefix is removed from each of the \paths\, + but the remaining sub-directory structure is reconstructed in the target + directory. + + The option ``\<^theory_text>\export_files paths\'' exports the specified files from the + temporary directory to the session database, \emph{after} invoking + \compile_body\. Entries may be decorated with ``\<^theory_text>\(exe)\'' to say that it is + a platform-specific executable program: the executable file-attribute will + be set, and on Windows the \<^verbatim>\.exe\ file-extension will be included; + ``\<^theory_text>\(executable)\'' only refers to the file-attribute, without special + treatment of the \<^verbatim>\.exe\ extension. + + The option ``\<^theory_text>\export_prefix path\'' specifies an extra path prefix for all + exports of \<^theory_text>\export_files\ above. \<^descr> \<^theory_text>\external_file name\ declares the formal dependency on the given file name, such that the Isabelle build process knows about it (see also @{cite - "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via \<^ML>\File.read\, without specific management by the Prover IDE. + "isabelle-system"}). This is required for any files mentioned in + \<^theory_text>\compile_generated_files / external_files\ above, in order to document + source dependencies properly. It is also possible to use \<^theory_text>\external_file\ + alone, e.g.\ when other Isabelle/ML tools use \<^ML>\File.read\, without + specific management of content by the Prover IDE. \ - section \Primitive specification elements\ subsection \Sorts\ diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Admin/build_release.scala Thu Apr 04 22:21:09 2019 +0200 @@ -653,7 +653,7 @@ } yield (bundle_info.name, bundle_info) val afp_link = - HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) + HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/General/path.ML Thu Apr 04 22:21:09 2019 +0200 @@ -43,6 +43,9 @@ val binding0: T -> binding val map_binding: (T -> T) -> binding -> binding val dest_binding: binding -> T * Position.T + val path_of_binding: binding -> T + val pos_of_binding: binding -> Position.T + val proper_binding: binding -> unit val implode_binding: binding -> string val explode_binding: string * Position.T -> binding val explode_binding0: string -> binding @@ -260,7 +263,7 @@ datatype binding = Binding of T * Position.T; fun binding (path, pos) = - if not (is_current path) andalso all_basic path then Binding (path, pos) + if all_basic path then Binding (path, pos) else error ("Bad path binding: " ^ print path ^ Position.here pos); fun binding0 path = binding (path, Position.none); @@ -268,8 +271,15 @@ fun map_binding f (Binding (path, pos)) = binding (f path, pos); fun dest_binding (Binding args) = args; +val path_of_binding = dest_binding #> #1; +val pos_of_binding = dest_binding #> #2; -val implode_binding = dest_binding #> #1 #> implode_path; +fun proper_binding binding = + if is_current (path_of_binding binding) + then error ("Empty path" ^ Position.here (pos_of_binding binding)) + else (); + +val implode_binding = path_of_binding #> implode_path; val explode_binding = binding o explode_pos; fun explode_binding0 s = explode_binding (s, Position.none); diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Isar/parse.ML Thu Apr 04 22:21:09 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 7b6add80e3a5 -r 06edf32c6057 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/PIDE/resources.ML Thu Apr 04 22:21:09 2019 +0200 @@ -34,9 +34,9 @@ val provide_file: Token.file -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val loaded_files_current: theory -> bool - val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T - val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T - val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T + val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T + val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T + val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T end; structure Resources: RESOURCES = @@ -242,11 +242,15 @@ (* formal check *) -fun formal_check check_file ctxt dir (name, pos) = +fun formal_check check_file ctxt opt_dir (name, pos) = let fun err msg = error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos Markup.language_path; + val dir = + (case opt_dir of + SOME dir => dir + | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = Path.append dir (Path.explode name) handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); @@ -262,11 +266,10 @@ local -fun document_antiq check = +fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => let - val dir = master_directory (Proof_Context.theory_of ctxt); - val _: Path.T = check ctxt dir (name, pos); + val _ = check ctxt NONE (name, pos); val latex = space_explode "/" name |> map Latex.output_ascii @@ -275,7 +278,7 @@ fun ML_antiq check = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => - check ctxt Path.current (name, pos) |> ML_Syntax.print_path); + check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); in diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Pure.thy Thu Apr 04 22:21:09 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" @@ -123,29 +124,46 @@ 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_theory = + (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- + Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); + 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_theory >> (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))); + + + val base_dir = + Scan.optional (\<^keyword>\(\ |-- + Parse.!!! (\<^keyword>\in\ |-- Parse.position Parse.path --| \<^keyword>\)\)) ("", Position.none); + + val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir; + + 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_theory -- + Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- + Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- + Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", 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 7b6add80e3a5 -r 06edf32c6057 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/System/isabelle_system.ML Thu Apr 04 22:21:09 2019 +0200 @@ -15,6 +15,7 @@ val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a + val bash_output_check: string -> string val bash_output: string -> string * int val bash: string -> int end; @@ -24,6 +25,11 @@ (* bash *) +fun bash_output_check s = + (case Bash.process s of + {rc = 0, out, ...} => (trim_line out) + | {err, ...} => error (trim_line err)); + fun bash_output s = let val {out, err, rc, ...} = Bash.process s; diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Thy/export.ML Thu Apr 04 22:21:09 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 (tap Path.proper_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 7b6add80e3a5 -r 06edf32c6057 src/Pure/Thy/sessions.ML --- a/src/Pure/Thy/sessions.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Thy/sessions.ML Thu Apr 04 22:21:09 2019 +0200 @@ -64,7 +64,7 @@ let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; - val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir; + val session_dir = Resources.check_dir ctxt NONE dir; val _ = (the_list parent @ sessions) |> List.app (fn arg => @@ -88,19 +88,19 @@ Resources.import_name session session_dir s handle ERROR msg => error (msg ^ Position.here pos); val theory_path = the_default node_name (Resources.known_theory theory_name); - val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos); + val _ = Resources.check_file ctxt (SOME Path.current) (Path.implode theory_path, pos); in () end); val _ = document_files |> List.app (fn (doc_dir, doc_files) => let - val dir = Resources.check_dir ctxt session_dir doc_dir; - val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files; + val dir = Resources.check_dir ctxt (SOME session_dir) doc_dir; + val _ = List.app (ignore o Resources.check_file ctxt (SOME dir)) doc_files; in () end); val _ = export_files |> List.app (fn ((export_dir, _), _) => - ignore (Resources.check_path ctxt session_dir export_dir)); + ignore (Resources.check_path ctxt (SOME session_dir) export_dir)); in () end)); end; diff -r 7b6add80e3a5 -r 06edf32c6057 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Pure/Tools/generated_files.ML Thu Apr 04 22:21:09 2019 +0200 @@ -7,10 +7,18 @@ 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 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 * 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 + 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 +28,22 @@ ({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 + val with_compile_dir: (Path.T -> unit) -> unit + val compile_generated_files: Proof.context -> + (Path.binding list * theory) list -> + (Path.T 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 -> + ((string * Position.T) list * bool option) list -> + string * Position.T -> Input.source -> unit end; structure Generated_Files: GENERATED_FILES = @@ -50,11 +73,11 @@ Name_Space.merge_tables (antiqs1, antiqs2)); ); - -(* files *) - fun add_files (binding, content) = - let val (path, pos) = Path.dest_binding binding in + let + val _ = Path.proper_binding binding; + val (path, pos) = Path.dest_binding binding; + in (Data.map o @{apply 3(1)}) (fn files => (case AList.lookup (op =) files path of SOME (pos', _) => @@ -62,34 +85,62 @@ | 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 file_markup (file: file) = (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 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)) => + {path = path, pos = pos, content = content}: file); -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_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 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 *) -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 +161,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,23 +213,103 @@ in implode (map expand input) end; -(* generate files *) + +(** Isar commands **) -fun generate_file_cmd ((file, pos), source) lthy = +(* generate_file *) + +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; + + +(* export_generated_files *) + +fun export_generated_files ctxt args = + let val thy = Proof_Context.theory_of ctxt in + (case map #1 (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); + + +(* 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 (files, base_dir) => + files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, 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 binding0 => + let + val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe); + val (path, pos) = Path.dest_binding binding; + 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) + (external |> map (fn (raw_files, raw_base_dir) => + let + val base_dir = Resources.check_dir ctxt NONE raw_base_dir; + fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s); + val files = map check raw_files; + in (files, base_dir) end)) + ((map o apfst o map) Path.explode_binding export) + (Path.explode_binding export_prefix) + source; + + (** concrete file types **) @@ -224,7 +355,7 @@ fun path_antiquotation binding check = antiquotation binding (Args.context -- Scan.lift (Parse.position Parse.path) >> - (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode))) + (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode))) (fn {file_type, argument, ...} => #make_string file_type argument); val _ = diff -r 7b6add80e3a5 -r 06edf32c6057 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Tools/Haskell/Haskell.thy Thu Apr 04 22:21:09 2019 +0200 @@ -1943,6 +1943,6 @@ return () \ -export_generated_files +export_generated_files _ end diff -r 7b6add80e3a5 -r 06edf32c6057 src/Tools/Haskell/Test.thy --- a/src/Tools/Haskell/Test.thy Thu Apr 04 16:38:45 2019 +0100 +++ b/src/Tools/Haskell/Test.thy Thu Apr 04 22:21:09 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",