--- a/src/HOL/Codegenerator_Test/Generate.thy Thu Jul 08 16:19:24 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy Thu Jul 08 16:19:24 2010 +0200
@@ -7,9 +7,23 @@
imports Candidates
begin
-export_code * in SML module_name Code_Test
- in OCaml module_name Code_Test file -
- in Haskell file -
- in Scala file -
+subsection {* Check whether generated code compiles *}
+
+text {*
+ If any of the @{text ML} ... check fails, inspect the code generated
+ by the previous @{text export_code} command.
+*}
+
+export_code "*" in SML module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+
+export_code "*" in OCaml module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+
+export_code "*" in Haskell module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+
+export_code "*" in Scala module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
end