--- 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
--- 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
--- 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 ***
--- 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} \<newline>
- @{syntax mixfix}? @'=' @{syntax term} + @'and');
+ @{syntax mixfix}? '=' @{syntax term} + @'and');
\<close>
The core of each interpretation command is a locale expression \<open>expr\<close>; the
@@ -1188,22 +1188,105 @@
\<close>
-section \<open>External file dependencies\<close>
+section \<open>Generated files and external files\<close>
text \<open>
- \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>\<open>export_files\<close> within session \<^verbatim>\<open>ROOT\<close> files, together with @{tool build}
+ option \<^verbatim>\<open>-e\<close>.
+
+ \begin{matharray}{rcll}
+ @{command_def "generate_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "export_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
+ @{command_def "compile_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
@{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
\end{matharray}
- \<^rail>\<open>@@{command external_file} @{syntax name} ';'?\<close>
+ \<^rail>\<open>
+ @@{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') \<newline>
+ (@'external_files' (external_files + @'and'))? \<newline>
+ (@'export_files' (export_files + @'and'))? \<newline>
+ (@'export_prefix' path)?
+ ;
+ external_files: (path+) (('(' @'in' path ')')?)
+ ;
+ export_files: (path+) (executable?)
+ ;
+ executable: '(' ('exe' | 'executable') ')'
+ ;
+ @@{command external_file} @{syntax name} ';'?
+ \<close>
+
+ \<^descr> \<^theory_text>\<open>generate_file path = content\<close> 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 \<open>content\<close> is a
+ string that is preprocessed according to rules of this file-type.
+
+ For example, Isabelle/Pure supports \<^verbatim>\<open>.hs\<close> as file-type for Haskell:
+ embedded cartouches are evaluated as Isabelle/ML expressions of type
+ \<^ML_type>\<open>string\<close>, the result is inlined in Haskell string syntax.
+
+ \<^descr> \<^theory_text>\<open>export_generated_files paths (in thy)\<close> 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>\<open>_\<close>''
+ (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>\<open>isabelle-export:\<close>''
+ (using the regular file-browser).
+
+ \<^descr> \<^theory_text>\<open>compile_generated_files paths (in thy) where compile_body\<close> retrieves
+ named generated files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into
+ a temporary directory, such that the \<open>compile_body\<close> may operate on them as
+ an ML function of type \<^ML_type>\<open>Path.T -> unit\<close>. This may create further
+ files, e.g.\ executables produced by a compiler that is invoked as external
+ process (e.g.\ via \<^ML>\<open>Isabelle_System.bash\<close>), or any other files.
+
+ The option ``\<^theory_text>\<open>external_files paths (in base_dir)\<close>'' copies files from the
+ physical file-system into the temporary directory, \emph{before} invoking
+ \<open>compile_body\<close>. The \<open>base_dir\<close> prefix is removed from each of the \<open>paths\<close>,
+ but the remaining sub-directory structure is reconstructed in the target
+ directory.
+
+ The option ``\<^theory_text>\<open>export_files paths\<close>'' exports the specified files from the
+ temporary directory to the session database, \emph{after} invoking
+ \<open>compile_body\<close>. Entries may be decorated with ``\<^theory_text>\<open>(exe)\<close>'' to say that it is
+ a platform-specific executable program: the executable file-attribute will
+ be set, and on Windows the \<^verbatim>\<open>.exe\<close> file-extension will be included;
+ ``\<^theory_text>\<open>(executable)\<close>'' only refers to the file-attribute, without special
+ treatment of the \<^verbatim>\<open>.exe\<close> extension.
+
+ The option ``\<^theory_text>\<open>export_prefix path\<close>'' specifies an extra path prefix for all
+ exports of \<^theory_text>\<open>export_files\<close> above.
\<^descr> \<^theory_text>\<open>external_file name\<close> 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>\<open>File.read\<close>, without specific management by the Prover IDE.
+ "isabelle-system"}). This is required for any files mentioned in
+ \<^theory_text>\<open>compile_generated_files / external_files\<close> above, in order to document
+ source dependencies properly. It is also possible to use \<^theory_text>\<open>external_file\<close>
+ alone, e.g.\ when other Isabelle/ML tools use \<^ML>\<open>File.read\<close>, without
+ specific management of content by the Prover IDE.
\<close>
-
section \<open>Primitive specification elements\<close>
subsection \<open>Sorts\<close>
--- 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)),
--- 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);
--- 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;
--- 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
--- 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>\<open>generate_file\<close>
"generate source file, with antiquotations"
- (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+ (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
>> Generated_Files.generate_file_cmd);
+
+ val files_in_theory =
+ (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
+ Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
+
val _ =
Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
- "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>\<open>(\<close> |--
+ Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.position Parse.path --| \<^keyword>\<open>)\<close>)) ("", 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>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
+
+ val export_files = Scan.repeat1 Parse.path_binding -- executable;
+
+ val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>compile_generated_files\<close>
+ "compile generated files and export results"
+ (Parse.and_list files_in_theory --
+ Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
+ Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
+ Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- 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\<close>
--- 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;
--- 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;
--- 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;
--- 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 _ =
--- 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 ()
\<close>
-export_generated_files
+export_generated_files _
end
--- 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>\<open>Haskell\<close> src_dir;
+ val files = Generated_Files.get_files \<^theory>\<open>Haskell\<close>;
+ 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",