merged
authorwenzelm
Thu Apr 04 22:21:09 2019 +0200 (6 months ago)
changeset 7005906edf32c6057
parent 70045 7b6add80e3a5
parent 70058 43acf9a457f0
child 70060 3e9394adcccd
merged
     1.1 --- a/Admin/components/components.sha1	Thu Apr 04 16:38:45 2019 +0100
     1.2 +++ b/Admin/components/components.sha1	Thu Apr 04 22:21:09 2019 +0200
     1.3 @@ -254,6 +254,7 @@
     1.4  b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf  sqlite-jdbc-3.18.0.tar.gz
     1.5  e56117a67ab01fb24c7fc054ede3160cefdac5f8  sqlite-jdbc-3.20.0.tar.gz
     1.6  27aeac6a91353d69f0438837798ac4ae6f9ff8c5  sqlite-jdbc-3.23.1.tar.gz
     1.7 +4d17611857fa3a93944c1f159c0fd2a161967aaf  sqlite-jdbc-3.27.2.1.tar.gz
     1.8  8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
     1.9  2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
    1.10  a2335d28b5b95d8d26500a53f1a9303fc5beaf36  ssh-java-20190323.tar.gz
     2.1 --- a/Admin/components/main	Thu Apr 04 16:38:45 2019 +0100
     2.2 +++ b/Admin/components/main	Thu Apr 04 22:21:09 2019 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  scala-2.12.8
     2.5  smbc-0.4.1
     2.6  spass-3.8ds-1
     2.7 -sqlite-jdbc-3.23.1
     2.8 +sqlite-jdbc-3.27.2.1
     2.9  ssh-java-20190323
    2.10  stack-1.9.3
    2.11  vampire-4.2.2
     3.1 --- a/NEWS	Thu Apr 04 16:38:45 2019 +0100
     3.2 +++ b/NEWS	Thu Apr 04 22:21:09 2019 +0200
     3.3 @@ -41,6 +41,13 @@
     3.4  need to provide a closed expression -- without trailing semicolon. Minor
     3.5  INCOMPATIBILITY.
     3.6  
     3.7 +* Commands 'generate_file', 'export_generated_files', and
     3.8 +'compile_generated_files' support a stateless (PIDE-conformant) model
     3.9 +for generated sources and compiled binaries of other languages. The
    3.10 +compilation processed is managed in Isabelle/ML, and results exported to
    3.11 +the session database for further use (e.g. with "isabelle export" or
    3.12 +"isabelle build -e").
    3.13 +
    3.14  
    3.15  *** Isabelle/jEdit Prover IDE ***
    3.16  
     4.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 16:38:45 2019 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 22:21:09 2019 +0200
     4.3 @@ -665,7 +665,7 @@
     4.4      ;
     4.5  
     4.6      definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
     4.7 -      @{syntax mixfix}? @'=' @{syntax term} + @'and');
     4.8 +      @{syntax mixfix}? '=' @{syntax term} + @'and');
     4.9    \<close>
    4.10  
    4.11    The core of each interpretation command is a locale expression \<open>expr\<close>; the
    4.12 @@ -1188,22 +1188,105 @@
    4.13  \<close>
    4.14  
    4.15  
    4.16 -section \<open>External file dependencies\<close>
    4.17 +section \<open>Generated files and external files\<close>
    4.18  
    4.19  text \<open>
    4.20 -  \begin{matharray}{rcl}
    4.21 +  Write access to the physical file-system is incompatible with the stateless
    4.22 +  model of processing Isabelle documents. To avoid bad effects, the theory
    4.23 +  context maintains a logical ``file-system'' for generated files, as a
    4.24 +  mapping of structured file-names to content. Names need to be unique for
    4.25 +  each theory node. When exporting generated files for other purposes, the
    4.26 +  (long) theory name is prefixed for extra qualification, but there are also
    4.27 +  means to smash overlong paths. See also @{cite "isabelle-system"} for
    4.28 +  \<^theory_text>\<open>export_files\<close> within session \<^verbatim>\<open>ROOT\<close> files, together with @{tool build}
    4.29 +  option \<^verbatim>\<open>-e\<close>.
    4.30 +
    4.31 +  \begin{matharray}{rcll}
    4.32 +    @{command_def "generate_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    4.33 +    @{command_def "export_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
    4.34 +    @{command_def "compile_generated_files"} & : & \<open>context \<rightarrow>\<close> \\
    4.35      @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
    4.36    \end{matharray}
    4.37  
    4.38 -  \<^rail>\<open>@@{command external_file} @{syntax name} ';'?\<close>
    4.39 +  \<^rail>\<open>
    4.40 +    @@{command generate_file} path '=' content
    4.41 +    ;
    4.42 +    path: @{syntax embedded}
    4.43 +    ;
    4.44 +    content: @{syntax embedded}
    4.45 +    ;
    4.46 +    @@{command export_generated_files} (files_in_theory + @'and')
    4.47 +    ;
    4.48 +    files_in_theory: (@'_' | (path+)) (('(' @'in' @{syntax name} ')')?)
    4.49 +    ;
    4.50 +    @@{command compile_generated_files} (files_in_theory + @'and') \<newline>
    4.51 +      (@'external_files' (external_files + @'and'))? \<newline>
    4.52 +      (@'export_files' (export_files + @'and'))? \<newline>
    4.53 +      (@'export_prefix' path)?
    4.54 +    ;
    4.55 +    external_files: (path+) (('(' @'in' path ')')?)
    4.56 +    ;
    4.57 +    export_files: (path+) (executable?)
    4.58 +    ;
    4.59 +    executable: '(' ('exe' | 'executable') ')'
    4.60 +    ;
    4.61 +    @@{command external_file} @{syntax name} ';'?
    4.62 +  \<close>
    4.63 +
    4.64 +  \<^descr> \<^theory_text>\<open>generate_file path = content\<close> augments the table of generated files
    4.65 +  within the current theory by a new entry: duplicates are not allowed. The
    4.66 +  name extension determines a pre-existent file-type; the \<open>content\<close> is a
    4.67 +  string that is preprocessed according to rules of this file-type.
    4.68 +
    4.69 +  For example, Isabelle/Pure supports \<^verbatim>\<open>.hs\<close> as file-type for Haskell:
    4.70 +  embedded cartouches are evaluated as Isabelle/ML expressions of type
    4.71 +  \<^ML_type>\<open>string\<close>, the result is inlined in Haskell string syntax.
    4.72 +
    4.73 +  \<^descr> \<^theory_text>\<open>export_generated_files paths (in thy)\<close> retrieves named generated files
    4.74 +  from the given theory (that needs be reachable via imports of the current
    4.75 +  one). By default, the current theory node is used. Using ``\<^verbatim>\<open>_\<close>''
    4.76 +  (underscore) instead of explicit path names refers to \emph{all} files of a
    4.77 +  theory node.
    4.78 +
    4.79 +  The overall list of files is prefixed with the respective (long) theory name
    4.80 +  and exported to the session database. In Isabelle/jEdit the result can be
    4.81 +  browsed via the virtual file-system with prefix ``\<^verbatim>\<open>isabelle-export:\<close>''
    4.82 +  (using the regular file-browser).
    4.83 +
    4.84 +  \<^descr> \<^theory_text>\<open>compile_generated_files paths (in thy) where compile_body\<close> retrieves
    4.85 +  named generated files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into
    4.86 +  a temporary directory, such that the \<open>compile_body\<close> may operate on them as
    4.87 +  an ML function of type \<^ML_type>\<open>Path.T -> unit\<close>. This may create further
    4.88 +  files, e.g.\ executables produced by a compiler that is invoked as external
    4.89 +  process (e.g.\ via \<^ML>\<open>Isabelle_System.bash\<close>), or any other files.
    4.90 +
    4.91 +  The option ``\<^theory_text>\<open>external_files paths (in base_dir)\<close>'' copies files from the
    4.92 +  physical file-system into the temporary directory, \emph{before} invoking
    4.93 +  \<open>compile_body\<close>. The \<open>base_dir\<close> prefix is removed from each of the \<open>paths\<close>,
    4.94 +  but the remaining sub-directory structure is reconstructed in the target
    4.95 +  directory.
    4.96 +
    4.97 +  The option ``\<^theory_text>\<open>export_files paths\<close>'' exports the specified files from the
    4.98 +  temporary directory to the session database, \emph{after} invoking
    4.99 +  \<open>compile_body\<close>. Entries may be decorated with ``\<^theory_text>\<open>(exe)\<close>'' to say that it is
   4.100 +  a platform-specific executable program: the executable file-attribute will
   4.101 +  be set, and on Windows the \<^verbatim>\<open>.exe\<close> file-extension will be included;
   4.102 +  ``\<^theory_text>\<open>(executable)\<close>'' only refers to the file-attribute, without special
   4.103 +  treatment of the \<^verbatim>\<open>.exe\<close> extension.
   4.104 +
   4.105 +  The option ``\<^theory_text>\<open>export_prefix path\<close>'' specifies an extra path prefix for all
   4.106 +  exports of \<^theory_text>\<open>export_files\<close> above.
   4.107  
   4.108    \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
   4.109    name, such that the Isabelle build process knows about it (see also @{cite
   4.110 -  "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.
   4.111 +  "isabelle-system"}). This is required for any files mentioned in
   4.112 +  \<^theory_text>\<open>compile_generated_files / external_files\<close> above, in order to document
   4.113 +  source dependencies properly. It is also possible to use \<^theory_text>\<open>external_file\<close>
   4.114 +  alone, e.g.\ when other Isabelle/ML tools use \<^ML>\<open>File.read\<close>, without
   4.115 +  specific management of content by the Prover IDE.
   4.116  \<close>
   4.117  
   4.118  
   4.119 -
   4.120  section \<open>Primitive specification elements\<close>
   4.121  
   4.122  subsection \<open>Sorts\<close>
     5.1 --- a/src/Pure/Admin/build_release.scala	Thu Apr 04 16:38:45 2019 +0100
     5.2 +++ b/src/Pure/Admin/build_release.scala	Thu Apr 04 22:21:09 2019 +0200
     5.3 @@ -653,7 +653,7 @@
     5.4          } yield (bundle_info.name, bundle_info)
     5.5  
     5.6        val afp_link =
     5.7 -        HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
     5.8 +        HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
     5.9  
    5.10        HTML.write_document(dir, "index.html",
    5.11          List(HTML.title(release.dist_name)),
     6.1 --- a/src/Pure/General/path.ML	Thu Apr 04 16:38:45 2019 +0100
     6.2 +++ b/src/Pure/General/path.ML	Thu Apr 04 22:21:09 2019 +0200
     6.3 @@ -43,6 +43,9 @@
     6.4    val binding0: T -> binding
     6.5    val map_binding: (T -> T) -> binding -> binding
     6.6    val dest_binding: binding -> T * Position.T
     6.7 +  val path_of_binding: binding -> T
     6.8 +  val pos_of_binding: binding -> Position.T
     6.9 +  val proper_binding: binding -> unit
    6.10    val implode_binding: binding -> string
    6.11    val explode_binding: string * Position.T -> binding
    6.12    val explode_binding0: string -> binding
    6.13 @@ -260,7 +263,7 @@
    6.14  datatype binding = Binding of T * Position.T;
    6.15  
    6.16  fun binding (path, pos) =
    6.17 -  if not (is_current path) andalso all_basic path then Binding (path, pos)
    6.18 +  if all_basic path then Binding (path, pos)
    6.19    else error ("Bad path binding: " ^ print path ^ Position.here pos);
    6.20  
    6.21  fun binding0 path = binding (path, Position.none);
    6.22 @@ -268,8 +271,15 @@
    6.23  fun map_binding f (Binding (path, pos)) = binding (f path, pos);
    6.24  
    6.25  fun dest_binding (Binding args) = args;
    6.26 +val path_of_binding = dest_binding #> #1;
    6.27 +val pos_of_binding = dest_binding #> #2;
    6.28  
    6.29 -val implode_binding = dest_binding #> #1 #> implode_path;
    6.30 +fun proper_binding binding =
    6.31 +  if is_current (path_of_binding binding)
    6.32 +  then error ("Empty path" ^ Position.here (pos_of_binding binding))
    6.33 +  else ();
    6.34 +
    6.35 +val implode_binding = path_of_binding #> implode_path;
    6.36  
    6.37  val explode_binding = binding o explode_pos;
    6.38  fun explode_binding0 s = explode_binding (s, Position.none);
     7.1 --- a/src/Pure/Isar/parse.ML	Thu Apr 04 16:38:45 2019 +0100
     7.2 +++ b/src/Pure/Isar/parse.ML	Thu Apr 04 22:21:09 2019 +0200
     7.3 @@ -70,6 +70,7 @@
     7.4    val embedded_position: (string * Position.T) parser
     7.5    val text: string parser
     7.6    val path: string parser
     7.7 +  val path_binding: (string * Position.T) parser
     7.8    val session_name: (string * Position.T) parser
     7.9    val theory_name: (string * Position.T) parser
    7.10    val liberal_name: string parser
    7.11 @@ -282,6 +283,7 @@
    7.12  val text = group (fn () => "text") (embedded || verbatim);
    7.13  
    7.14  val path = group (fn () => "file name/path specification") embedded;
    7.15 +val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
    7.16  
    7.17  val session_name = group (fn () => "session name") name_position;
    7.18  val theory_name = group (fn () => "theory name") name_position;
     8.1 --- a/src/Pure/PIDE/resources.ML	Thu Apr 04 16:38:45 2019 +0100
     8.2 +++ b/src/Pure/PIDE/resources.ML	Thu Apr 04 22:21:09 2019 +0200
     8.3 @@ -34,9 +34,9 @@
     8.4    val provide_file: Token.file -> theory -> theory
     8.5    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     8.6    val loaded_files_current: theory -> bool
     8.7 -  val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
     8.8 -  val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
     8.9 -  val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
    8.10 +  val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T
    8.11 +  val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T
    8.12 +  val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T
    8.13  end;
    8.14  
    8.15  structure Resources: RESOURCES =
    8.16 @@ -242,11 +242,15 @@
    8.17  
    8.18  (* formal check *)
    8.19  
    8.20 -fun formal_check check_file ctxt dir (name, pos) =
    8.21 +fun formal_check check_file ctxt opt_dir (name, pos) =
    8.22    let
    8.23      fun err msg = error (msg ^ Position.here pos);
    8.24  
    8.25      val _ = Context_Position.report ctxt pos Markup.language_path;
    8.26 +    val dir =
    8.27 +      (case opt_dir of
    8.28 +        SOME dir => dir
    8.29 +      | NONE => master_directory (Proof_Context.theory_of ctxt));
    8.30      val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
    8.31      val _ = Path.expand path handle ERROR msg => err msg;
    8.32      val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    8.33 @@ -262,11 +266,10 @@
    8.34  
    8.35  local
    8.36  
    8.37 -fun document_antiq check =
    8.38 +fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) =
    8.39    Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    8.40      let
    8.41 -      val dir = master_directory (Proof_Context.theory_of ctxt);
    8.42 -      val _: Path.T = check ctxt dir (name, pos);
    8.43 +      val _ = check ctxt NONE (name, pos);
    8.44        val latex =
    8.45          space_explode "/" name
    8.46          |> map Latex.output_ascii
    8.47 @@ -275,7 +278,7 @@
    8.48  
    8.49  fun ML_antiq check =
    8.50    Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    8.51 -    check ctxt Path.current (name, pos) |> ML_Syntax.print_path);
    8.52 +    check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path);
    8.53  
    8.54  in
    8.55  
     9.1 --- a/src/Pure/Pure.thy	Thu Apr 04 16:38:45 2019 +0100
     9.2 +++ b/src/Pure/Pure.thy	Thu Apr 04 22:21:09 2019 +0200
     9.3 @@ -23,6 +23,7 @@
     9.4    and "external_file" "bibtex_file" :: thy_load
     9.5    and "generate_file" :: thy_decl
     9.6    and "export_generated_files" :: diag
     9.7 +  and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
     9.8    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     9.9    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    9.10    and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
    9.11 @@ -123,29 +124,46 @@
    9.12    val _ =
    9.13      Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
    9.14        "generate source file, with antiquotations"
    9.15 -      (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    9.16 +      (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    9.17          >> Generated_Files.generate_file_cmd);
    9.18  
    9.19 +
    9.20 +  val files_in_theory =
    9.21 +    (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
    9.22 +      Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
    9.23 +
    9.24    val _ =
    9.25      Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
    9.26 -      "export generated files from this or other theories"
    9.27 -      (Scan.repeat Parse.name_position >> (fn names =>
    9.28 +      "export generated files from given theories"
    9.29 +      (Parse.and_list1 files_in_theory >> (fn args =>
    9.30          Toplevel.keep (fn st =>
    9.31 -          let
    9.32 -            val ctxt = Toplevel.context_of st;
    9.33 -            val thy = Toplevel.theory_of st;
    9.34 -            val other_thys =
    9.35 -              if null names then [thy]
    9.36 -              else map (Theory.check {long = false} ctxt) names;
    9.37 -            val paths = Generated_Files.export_files thy other_thys;
    9.38 -          in
    9.39 -            if not (null paths) then
    9.40 -              (writeln (Export.message thy Path.current);
    9.41 -               writeln (cat_lines (paths |> map (fn (path, pos) =>
    9.42 -                Markup.markup (Markup.entityN, Position.def_properties_of pos)
    9.43 -                  (quote (Path.implode path))))))
    9.44 -            else ()
    9.45 -          end)));
    9.46 +          Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)));
    9.47 +
    9.48 +
    9.49 +  val base_dir =
    9.50 +    Scan.optional (\<^keyword>\<open>(\<close> |--
    9.51 +      Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.position Parse.path --| \<^keyword>\<open>)\<close>)) ("", Position.none);
    9.52 +
    9.53 +  val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir;
    9.54 +
    9.55 +  val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false;
    9.56 +  val executable = \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
    9.57 +
    9.58 +  val export_files = Scan.repeat1 Parse.path_binding -- executable;
    9.59 +
    9.60 +  val _ =
    9.61 +    Outer_Syntax.command \<^command_keyword>\<open>compile_generated_files\<close>
    9.62 +      "compile generated files and export results"
    9.63 +      (Parse.and_list files_in_theory --
    9.64 +        Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
    9.65 +        Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
    9.66 +        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("", Position.none) --
    9.67 +        (Parse.where_ |-- Parse.!!! Parse.ML_source)
    9.68 +        >> (fn ((((args, external), export), export_prefix), source) =>
    9.69 +          Toplevel.keep (fn st =>
    9.70 +            Generated_Files.compile_generated_files_cmd
    9.71 +              (Toplevel.context_of st) args external export export_prefix source)));
    9.72 +
    9.73  in end\<close>
    9.74  
    9.75  
    10.1 --- a/src/Pure/System/isabelle_system.ML	Thu Apr 04 16:38:45 2019 +0100
    10.2 +++ b/src/Pure/System/isabelle_system.ML	Thu Apr 04 22:21:09 2019 +0200
    10.3 @@ -15,6 +15,7 @@
    10.4    val create_tmp_path: string -> string -> Path.T
    10.5    val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    10.6    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    10.7 +  val bash_output_check: string -> string
    10.8    val bash_output: string -> string * int
    10.9    val bash: string -> int
   10.10  end;
   10.11 @@ -24,6 +25,11 @@
   10.12  
   10.13  (* bash *)
   10.14  
   10.15 +fun bash_output_check s =
   10.16 +  (case Bash.process s of
   10.17 +    {rc = 0, out, ...} => (trim_line out)
   10.18 +  | {err, ...} => error (trim_line err));
   10.19 +
   10.20  fun bash_output s =
   10.21    let
   10.22      val {out, err, rc, ...} = Bash.process s;
    11.1 --- a/src/Pure/Thy/export.ML	Thu Apr 04 16:38:45 2019 +0100
    11.2 +++ b/src/Pure/Thy/export.ML	Thu Apr 04 22:21:09 2019 +0200
    11.3 @@ -6,6 +6,7 @@
    11.4  
    11.5  signature EXPORT =
    11.6  sig
    11.7 +  val report_export: theory -> Path.binding -> unit
    11.8    type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}
    11.9    val export_params: params -> string list -> unit
   11.10    val export: theory -> Path.binding -> string list -> unit
   11.11 @@ -21,25 +22,24 @@
   11.12  
   11.13  (* export *)
   11.14  
   11.15 +fun report_export thy binding =
   11.16 +  let
   11.17 +    val theory_name = Context.theory_long_name thy;
   11.18 +    val (path, pos) = Path.dest_binding binding;
   11.19 +    val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
   11.20 +  in Context_Position.report_generic (Context.Theory thy) pos markup end;
   11.21 +
   11.22  type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
   11.23  
   11.24  fun export_params ({theory = thy, binding, executable, compress}: params) blob =
   11.25 -  let
   11.26 -    val theory_name = Context.theory_long_name thy;
   11.27 -    val name = Path.implode_binding binding;
   11.28 -    val (path, pos) = Path.dest_binding binding;
   11.29 -    val _ =
   11.30 -      Context_Position.report_generic (Context.Theory thy) pos
   11.31 -        (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)));
   11.32 -  in
   11.33 -    (Output.try_protocol_message o Markup.export)
   11.34 -     {id = Position.get_id (Position.thread_data ()),
   11.35 -      serial = serial (),
   11.36 -      theory_name = theory_name,
   11.37 -      name = name,
   11.38 -      executable = executable,
   11.39 -      compress = compress} blob
   11.40 -  end;
   11.41 + (report_export thy binding;
   11.42 +  (Output.try_protocol_message o Markup.export)
   11.43 +   {id = Position.get_id (Position.thread_data ()),
   11.44 +    serial = serial (),
   11.45 +    theory_name = Context.theory_long_name thy,
   11.46 +    name = Path.implode_binding (tap Path.proper_binding binding),
   11.47 +    executable = executable,
   11.48 +    compress = compress} blob);
   11.49  
   11.50  fun export thy binding blob =
   11.51    export_params {theory = thy, binding = binding, executable = false, compress = true} blob;
    12.1 --- a/src/Pure/Thy/sessions.ML	Thu Apr 04 16:38:45 2019 +0100
    12.2 +++ b/src/Pure/Thy/sessions.ML	Thu Apr 04 22:21:09 2019 +0200
    12.3 @@ -64,7 +64,7 @@
    12.4        let
    12.5          val ctxt = Toplevel.context_of state;
    12.6          val thy = Toplevel.theory_of state;
    12.7 -        val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
    12.8 +        val session_dir = Resources.check_dir ctxt NONE dir;
    12.9  
   12.10          val _ =
   12.11            (the_list parent @ sessions) |> List.app (fn arg =>
   12.12 @@ -88,19 +88,19 @@
   12.13                  Resources.import_name session session_dir s
   12.14                    handle ERROR msg => error (msg ^ Position.here pos);
   12.15                val theory_path = the_default node_name (Resources.known_theory theory_name);
   12.16 -              val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos);
   12.17 +              val _ = Resources.check_file ctxt (SOME Path.current) (Path.implode theory_path, pos);
   12.18              in () end);
   12.19  
   12.20          val _ =
   12.21            document_files |> List.app (fn (doc_dir, doc_files) =>
   12.22              let
   12.23 -              val dir = Resources.check_dir ctxt session_dir doc_dir;
   12.24 -              val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
   12.25 +              val dir = Resources.check_dir ctxt (SOME session_dir) doc_dir;
   12.26 +              val _ = List.app (ignore o Resources.check_file ctxt (SOME dir)) doc_files;
   12.27              in () end);
   12.28  
   12.29          val _ =
   12.30            export_files |> List.app (fn ((export_dir, _), _) =>
   12.31 -            ignore (Resources.check_path ctxt session_dir export_dir));
   12.32 +            ignore (Resources.check_path ctxt (SOME session_dir) export_dir));
   12.33        in () end));
   12.34  
   12.35  end;
    13.1 --- a/src/Pure/Tools/generated_files.ML	Thu Apr 04 16:38:45 2019 +0100
    13.2 +++ b/src/Pure/Tools/generated_files.ML	Thu Apr 04 22:21:09 2019 +0200
    13.3 @@ -7,10 +7,18 @@
    13.4  signature GENERATED_FILES =
    13.5  sig
    13.6    val add_files: Path.binding * string -> theory -> theory
    13.7 -  val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
    13.8 -  val write_files: theory -> Path.T -> (Path.T * Position.T) list
    13.9 -  val export_files: theory -> theory list -> (Path.T * Position.T) list
   13.10 -  val the_file_content: theory -> Path.T -> string
   13.11 +  type file = {path: Path.T, pos: Position.T, content: string}
   13.12 +  val file_binding: file -> Path.binding
   13.13 +  val file_markup: file -> Markup.T
   13.14 +  val print_file: file -> string
   13.15 +  val report_file: Proof.context -> Position.T -> file -> unit
   13.16 +  val get_files: theory -> file list
   13.17 +  val get_file: theory -> Path.binding -> file
   13.18 +  val get_files_in: Path.binding list * theory -> (file * Position.T) list
   13.19 +  val check_files_in: Proof.context ->
   13.20 +    (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
   13.21 +  val write_file: Path.T -> file -> unit
   13.22 +  val export_file: theory -> file -> unit
   13.23    type file_type =
   13.24      {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   13.25    val file_type:
   13.26 @@ -20,7 +28,22 @@
   13.27      ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
   13.28      theory -> theory
   13.29    val set_string: string -> Proof.context -> Proof.context
   13.30 +  val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
   13.31    val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
   13.32 +  val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
   13.33 +  val export_generated_files_cmd: Proof.context ->
   13.34 +    ((string * Position.T) list * (string * Position.T) option) list -> unit
   13.35 +  val with_compile_dir: (Path.T -> unit) -> unit
   13.36 +  val compile_generated_files: Proof.context ->
   13.37 +    (Path.binding list * theory) list ->
   13.38 +    (Path.T list * Path.T) list ->
   13.39 +    (Path.binding list * bool option) list ->
   13.40 +    Path.binding -> Input.source -> unit
   13.41 +  val compile_generated_files_cmd: Proof.context ->
   13.42 +    ((string * Position.T) list * (string * Position.T) option) list ->
   13.43 +    ((string * Position.T) list * (string * Position.T)) list ->
   13.44 +    ((string * Position.T) list * bool option) list ->
   13.45 +    string * Position.T -> Input.source -> unit
   13.46  end;
   13.47  
   13.48  structure Generated_Files: GENERATED_FILES =
   13.49 @@ -50,11 +73,11 @@
   13.50       Name_Space.merge_tables (antiqs1, antiqs2));
   13.51  );
   13.52  
   13.53 -
   13.54 -(* files *)
   13.55 -
   13.56  fun add_files (binding, content) =
   13.57 -  let val (path, pos) = Path.dest_binding binding in
   13.58 +  let
   13.59 +    val _ = Path.proper_binding binding;
   13.60 +    val (path, pos) = Path.dest_binding binding;
   13.61 +  in
   13.62      (Data.map o @{apply 3(1)}) (fn files =>
   13.63        (case AList.lookup (op =) files path of
   13.64          SOME (pos', _) =>
   13.65 @@ -62,34 +85,62 @@
   13.66        | NONE => (path, (pos, content)) :: files))
   13.67    end;
   13.68  
   13.69 -val get_files =
   13.70 -  map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}) o
   13.71 -    rev o #1 o Data.get;
   13.72 +
   13.73 +(* get files *)
   13.74 +
   13.75 +type file = {path: Path.T, pos: Position.T, content: string};
   13.76 +
   13.77 +fun file_binding (file: file) = Path.binding (#path file, #pos file);
   13.78 +
   13.79 +fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file));
   13.80  
   13.81 -fun write_files thy dir =
   13.82 -  get_files thy |> map (fn {path, pos, content} =>
   13.83 -    let
   13.84 -      val path' = Path.expand (Path.append dir path);
   13.85 -      val _ = Isabelle_System.mkdirs (Path.dir path');
   13.86 -      val _ = File.generate path' content;
   13.87 -    in (path, pos) end);
   13.88 +fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file)));
   13.89 +
   13.90 +fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file);
   13.91 +
   13.92 +
   13.93 +fun get_files thy =
   13.94 +  Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
   13.95 +    {path = path, pos = pos, content = content}: file);
   13.96  
   13.97 -fun export_files thy other_thys =
   13.98 -  other_thys |> maps (fn other_thy =>
   13.99 -    get_files other_thy |> map (fn {path, pos, content} =>
  13.100 -      (Export.export thy (Path.binding (path, pos)) [content]; (path, pos))));
  13.101 +fun get_file thy binding =
  13.102 +  let val (path, pos) = Path.dest_binding binding in
  13.103 +    (case find_first (fn file => #path file = path) (get_files thy) of
  13.104 +      SOME file => file
  13.105 +    | NONE =>
  13.106 +        error ("Missing generated file " ^ Path.print path ^
  13.107 +          " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
  13.108 +  end;
  13.109 +
  13.110 +fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy)
  13.111 +  | get_files_in (files, thy) =
  13.112 +      map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files;
  13.113 +
  13.114 +
  13.115 +(* check and output files *)
  13.116  
  13.117 -fun the_file_content thy path =
  13.118 -  (case find_first (fn file => #path file = path) (get_files thy) of
  13.119 -    SOME {content, ...} => content
  13.120 -  | NONE =>
  13.121 -      error ("Missing generated file " ^ Path.print path ^
  13.122 -        " in theory " ^ quote (Context.theory_long_name thy)));
  13.123 +fun check_files_in ctxt (files, opt_thy) =
  13.124 +  let
  13.125 +    val thy =
  13.126 +      (case opt_thy of
  13.127 +        SOME name => Theory.check {long = false} ctxt name
  13.128 +      | NONE => Proof_Context.theory_of ctxt);
  13.129 +  in (map Path.explode_binding files, thy) end;
  13.130 +
  13.131 +fun write_file dir (file: file) =
  13.132 +  let
  13.133 +    val path = Path.expand (Path.append dir (#path file));
  13.134 +    val _ = Isabelle_System.mkdirs (Path.dir path);
  13.135 +    val _ = File.generate path (#content file);
  13.136 +  in () end;
  13.137 +
  13.138 +fun export_file thy (file: file) =
  13.139 +  Export.export thy (file_binding file) [#content file];
  13.140  
  13.141  
  13.142  (* file types *)
  13.143  
  13.144 -fun the_file_type thy ext =
  13.145 +fun get_file_type thy ext =
  13.146    if ext = "" then error "Bad file extension"
  13.147    else
  13.148      (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
  13.149 @@ -110,7 +161,7 @@
  13.150      val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
  13.151  
  13.152      val _ =
  13.153 -      (case try (#name o the_file_type thy) ext of
  13.154 +      (case try (#name o get_file_type thy) ext of
  13.155          NONE => ()
  13.156        | SOME name' =>
  13.157            error ("Extension " ^ quote ext ^ " already registered for file type " ^
  13.158 @@ -162,23 +213,103 @@
  13.159    in implode (map expand input) end;
  13.160  
  13.161  
  13.162 -(* generate files *)
  13.163 +
  13.164 +(** Isar commands **)
  13.165  
  13.166 -fun generate_file_cmd ((file, pos), source) lthy =
  13.167 +(* generate_file *)
  13.168 +
  13.169 +fun generate_file (binding, source) lthy =
  13.170    let
  13.171      val thy = Proof_Context.theory_of lthy;
  13.172  
  13.173 -    val path = Path.explode file;
  13.174 -    val binding = Path.binding (path, pos);
  13.175 +    val (path, pos) = Path.dest_binding binding;
  13.176      val file_type =
  13.177 -      the_file_type thy (#2 (Path.split_ext path))
  13.178 +      get_file_type thy (#2 (Path.split_ext path))
  13.179          handle ERROR msg => error (msg ^ Position.here pos);
  13.180  
  13.181      val header = #make_comment file_type " generated by Isabelle ";
  13.182      val content = header ^ "\n" ^ read_source lthy file_type source;
  13.183    in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
  13.184  
  13.185 - 
  13.186 +fun generate_file_cmd (file, source) lthy =
  13.187 +  generate_file (Path.explode_binding file, source) lthy;
  13.188 +
  13.189 +
  13.190 +(* export_generated_files *)
  13.191 +
  13.192 +fun export_generated_files ctxt args =
  13.193 +  let val thy = Proof_Context.theory_of ctxt in
  13.194 +    (case map #1 (maps get_files_in args) of
  13.195 +      [] => ()
  13.196 +    | files =>
  13.197 +       (List.app (export_file thy) files;
  13.198 +        writeln (Export.message thy Path.current);
  13.199 +        writeln (cat_lines (map (prefix "  " o print_file) files))))
  13.200 +  end;
  13.201 +
  13.202 +fun export_generated_files_cmd ctxt args =
  13.203 +  export_generated_files ctxt (map (check_files_in ctxt) args);
  13.204 +
  13.205 +
  13.206 +(* compile_generated_files *)
  13.207 +
  13.208 +val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
  13.209 +
  13.210 +fun with_compile_dir body : unit =
  13.211 +  body (Path.explode (Config.get (Context.the_local_context ()) compile_dir));
  13.212 +
  13.213 +fun compile_generated_files ctxt args external export export_prefix source =
  13.214 +  Isabelle_System.with_tmp_dir "compile" (fn dir =>
  13.215 +    let
  13.216 +      val thy = Proof_Context.theory_of ctxt;
  13.217 +
  13.218 +      val files = maps get_files_in args;
  13.219 +      val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
  13.220 +      val _ = List.app (write_file dir o #1) files;
  13.221 +      val _ =
  13.222 +        external |> List.app (fn (files, base_dir) =>
  13.223 +          files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
  13.224 +      val _ =
  13.225 +        ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
  13.226 +          ML_Compiler.flags (Input.pos_of source)
  13.227 +          (ML_Lex.read "Generated_Files.with_compile_dir (" @
  13.228 +            ML_Lex.read_source source @ ML_Lex.read ")");
  13.229 +      val _ =
  13.230 +        export |> List.app (fn (bindings, executable) =>
  13.231 +          bindings |> List.app (fn binding0 =>
  13.232 +            let
  13.233 +              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
  13.234 +              val (path, pos) = Path.dest_binding binding;
  13.235 +              val content =
  13.236 +                (case try File.read (Path.append dir path) of
  13.237 +                  SOME context => context
  13.238 +                | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
  13.239 +              val _ = Export.report_export thy export_prefix;
  13.240 +              val binding' =
  13.241 +                Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
  13.242 +            in
  13.243 +              (if is_some executable then Export.export_executable else Export.export)
  13.244 +                thy binding' [content]
  13.245 +            end));
  13.246 +      val _ =
  13.247 +        if null export then ()
  13.248 +        else writeln (Export.message thy (Path.path_of_binding export_prefix));
  13.249 +    in () end);
  13.250 +
  13.251 +fun compile_generated_files_cmd ctxt args external export export_prefix source =
  13.252 +  compile_generated_files ctxt
  13.253 +    (map (check_files_in ctxt) args)
  13.254 +    (external |> map (fn (raw_files, raw_base_dir) =>
  13.255 +      let
  13.256 +        val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
  13.257 +        fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s);
  13.258 +        val files = map check raw_files;
  13.259 +      in (files, base_dir) end))
  13.260 +    ((map o apfst o map) Path.explode_binding export)
  13.261 +    (Path.explode_binding export_prefix)
  13.262 +    source;
  13.263 +
  13.264 +
  13.265  
  13.266  (** concrete file types **)
  13.267  
  13.268 @@ -224,7 +355,7 @@
  13.269  fun path_antiquotation binding check =
  13.270    antiquotation binding
  13.271      (Args.context -- Scan.lift (Parse.position Parse.path) >>
  13.272 -      (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
  13.273 +      (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode)))
  13.274      (fn {file_type, argument, ...} => #make_string file_type argument);
  13.275  
  13.276  val _ =
    14.1 --- a/src/Tools/Haskell/Haskell.thy	Thu Apr 04 16:38:45 2019 +0100
    14.2 +++ b/src/Tools/Haskell/Haskell.thy	Thu Apr 04 22:21:09 2019 +0200
    14.3 @@ -1943,6 +1943,6 @@
    14.4        return ()
    14.5  \<close>
    14.6  
    14.7 -export_generated_files
    14.8 +export_generated_files _
    14.9  
   14.10  end
    15.1 --- a/src/Tools/Haskell/Test.thy	Thu Apr 04 16:38:45 2019 +0100
    15.2 +++ b/src/Tools/Haskell/Test.thy	Thu Apr 04 22:21:09 2019 +0200
    15.3 @@ -11,10 +11,11 @@
    15.4    Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
    15.5      let
    15.6        val src_dir = Path.append tmp_dir (Path.explode "src");
    15.7 -      val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
    15.8 +      val files = Generated_Files.get_files \<^theory>\<open>Haskell\<close>;
    15.9 +      val _ = List.app (Generated_Files.write_file src_dir) files;
   15.10  
   15.11        val modules = files
   15.12 -        |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
   15.13 +        |> map (#path #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
   15.14        val _ =
   15.15          GHC.new_project tmp_dir
   15.16            {name = "isabelle",