--- a/NEWS Tue Apr 09 10:28:17 2019 +0200
+++ b/NEWS Tue Apr 09 10:51:35 2019 +0200
@@ -265,9 +265,8 @@
eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
\<close>
-The ML function Generate_File.generate writes all generated files from a
-given theory to the file-system, e.g. a temporary directory where some
-external compiler is applied.
+See also commands 'export_generated_files' and 'compile_generated_files'
+to use the results.
* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
--- a/src/Tools/Haskell/Test.thy Tue Apr 09 10:28:17 2019 +0200
+++ b/src/Tools/Haskell/Test.thy Tue Apr 09 10:51:35 2019 +0200
@@ -4,29 +4,24 @@
section \<open>Test build of Isabelle/Haskell modules\<close>
-theory Test imports Haskell
+theory Test
+ imports Haskell
begin
-ML \<open>
- Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
+compile_generated_files _ (in Haskell)
+ where \<open>fn dir =>
let
- val src_dir = Path.append tmp_dir (Path.explode "src");
- val files = Generated_Files.get_files \<^theory>\<open>Haskell\<close>;
- val _ = List.app (Generated_Files.write_file src_dir) files;
-
- val modules = files
+ val modules =
+ Generated_Files.get_files \<^theory>\<open>Haskell\<close>
|> map (#path #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
val _ =
- GHC.new_project tmp_dir
+ GHC.new_project dir
{name = "isabelle",
depends =
["bytestring", "containers", "network", "split", "threads", "utf8-string", "uuid"],
modules = modules};
-
- val (out, rc) =
- Isabelle_System.bash_output
- (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
- in if rc = 0 then writeln out else error out end)
-\<close>
+ in
+ writeln (Generated_Files.execute dir \<open>Build\<close> "mv Isabelle src && isabelle ghc_stack build")
+ end\<close>
end