merged
authorwenzelm
Thu, 04 Apr 2019 22:21:09 +0200
changeset 70241 06edf32c6057
parent 70227 7b6add80e3a5 (current diff)
parent 70240 43acf9a457f0 (diff)
child 70242 3e9394adcccd
merged
--- 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",