export generated files;

--- a/src/Pure/Tools/generated_files.ML	Fri Jan 11 10:59:21 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 11 11:05:36 2019 +0100
@@ -9,6 +9,7 @@
   val add_files: (Path.T * Position.T) * string -> theory -> theory
   val get_files: theory -> (Path.T * string) list
   val write_files: theory -> Path.T -> Path.T list
+  val export_files: theory -> Path.T list
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
@@ -76,6 +77,9 @@
       val _ = File.generate path' text;
     in path end);
 
+fun export_files thy =
+  get_files thy |> map (fn (path, text) => (Export.export thy (Path.implode path) [text]; path));
+
 
 (* file types *)
 

--- a/src/Tools/Haskell/Haskell.thy	Fri Jan 11 10:59:21 2019 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Fri Jan 11 11:05:36 2019 +0100
@@ -1924,4 +1924,6 @@
       return ()
 \<close>
 
+ML_command \<open>Generated_Files.export_files \<^theory>\<close>
+
 end