# HG changeset patch
# User wenzelm
# Date 1547579033 -3600
# Node ID fd86ed39aea4a0412f6b4b22d4b62afdf51379b8
# Parent  a03a63b81f446eafc88b91b29cf6eeed4a080dd9
added command 'export_generated_files';
clarified signature;

diff -r a03a63b81f44 -r fd86ed39aea4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Pure/Pure.thy	Tue Jan 15 20:03:53 2019 +0100
@@ -22,6 +22,7 @@
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   and "external_file" "bibtex_file" :: thy_load
   and "generate_file" :: thy_decl
+  and "export_generated_files" :: diag
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
   and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
@@ -125,6 +126,26 @@
       (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
         >> Generated_Files.generate_file_cmd);
 
+  val _ =
+    Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
+      "export generated files from this or other theories"
+      (Scan.repeat Parse.name_position >> (fn names =>
+        Toplevel.keep (fn st =>
+          let
+            val ctxt = Toplevel.context_of st;
+            val thy = Toplevel.theory_of st;
+            val other_thys =
+              if null names then [thy]
+              else map (Theory.check {long = false} ctxt) names;
+            val paths = Generated_Files.export_files thy other_thys;
+          in
+            if not (null paths) then
+              (writeln (Export.message thy "");
+               writeln (cat_lines (paths |> map (fn (path, pos) =>
+                Markup.markup (Markup.entityN, Position.def_properties_of pos)
+                  (quote (Path.implode path))))))
+            else ()
+          end)));
 in end\<close>
 
 
diff -r a03a63b81f44 -r fd86ed39aea4 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Pure/Tools/generated_files.ML	Tue Jan 15 20:03:53 2019 +0100
@@ -7,9 +7,9 @@
 signature GENERATED_FILES =
 sig
   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
+  val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
+  val write_files: theory -> Path.T -> (Path.T * Position.T) list
+  val export_files: theory -> theory list -> (Path.T * Position.T) list
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
@@ -67,18 +67,21 @@
       | NONE => (path, (pos, text)) :: files))
   end;
 
-val get_files = map (apsnd #2) o rev o #1 o Data.get;
+val get_files =
+  map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
 
 fun write_files thy dir =
-  get_files thy |> map (fn (path, text) =>
+  get_files thy |> map (fn {path, pos, text} =>
     let
       val path' = Path.expand (Path.append dir path);
       val _ = Isabelle_System.mkdirs (Path.dir path');
       val _ = File.generate path' text;
-    in path end);
+    in (path, pos) end);
 
-fun export_files thy =
-  get_files thy |> map (fn (path, text) => (Export.export thy (Path.implode path) [text]; path));
+fun export_files thy other_thys =
+  other_thys |> maps (fn other_thy =>
+    get_files other_thy |> map (fn {path, pos, text} =>
+      (Export.export thy (Path.implode path) [text]; (path, pos))));
 
 
 (* file types *)
diff -r a03a63b81f44 -r fd86ed39aea4 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Tools/Haskell/Haskell.thy	Tue Jan 15 20:03:53 2019 +0100
@@ -1924,6 +1924,6 @@
       return ()
 \<close>
 
-ML_command \<open>Generated_Files.export_files \<^theory>\<close>
+export_generated_files
 
 end
diff -r a03a63b81f44 -r fd86ed39aea4 src/Tools/Haskell/Test.thy
--- a/src/Tools/Haskell/Test.thy	Mon Jan 14 18:35:03 2019 +0000
+++ b/src/Tools/Haskell/Test.thy	Tue Jan 15 20:03:53 2019 +0100
@@ -14,7 +14,7 @@
       val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
 
       val modules = files
-        |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
+        |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
       val _ =
         GHC.new_project tmp_dir
           {name = "isabelle",