# HG changeset patch
# User wenzelm
# Date 1547201136 -3600
# Node ID a2fbfdc5e62d18bbc0ea25556793faa4d5875592
# Parent  3e26471d6d0188ab53fba9f2497da966d60eb8d5
export generated files;

diff -r 3e26471d6d01 -r a2fbfdc5e62d src/Pure/Tools/generated_files.ML
--- 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 *)
 
diff -r 3e26471d6d01 -r a2fbfdc5e62d src/Tools/Haskell/Haskell.thy
--- 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