# HG changeset patch
# User wenzelm
# Date 1554799895 -7200
# Node ID 4f936de6d9b8559a64fada7ed4bd30c0382e15e6
# Parent  093ab1a99eb6123930b10326c512acaf7f4b6d52
tuned -- prefer Isar command 'compile_generated_files';

diff -r 093ab1a99eb6 -r 4f936de6d9b8 NEWS
--- 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"
diff -r 093ab1a99eb6 -r 4f936de6d9b8 src/Tools/Haskell/Test.thy
--- 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