# HG changeset patch
# User wenzelm
# Date 1658408508 -7200
# Node ID 07cd3b243c6900edecd63bbc2f97123c14f50a65
# Parent  49444d7f8337f20f1ae27d5ec42aee41e8862f58
clarified signature;

diff -r 49444d7f8337 -r 07cd3b243c69 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Thu Jul 21 14:29:37 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Jul 21 15:01:48 2022 +0200
@@ -33,6 +33,9 @@
   val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
   val export_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list -> unit
+  val check_external_files: Proof.context ->
+    Input.source list * Input.source -> Path.T list * Path.T
+  val get_external_files: Path.T -> Path.T list * Path.T -> unit
   val with_compile_dir: (Path.T -> unit) -> unit
   val compile_generated_files: Proof.context ->
     (Path.binding list * theory) list ->
@@ -272,6 +275,21 @@
   export_generated_files ctxt (map (check_files_in ctxt) args);
 
 
+(* external files *)
+
+fun check_external_files ctxt (raw_files, raw_base_dir) =
+  let
+    val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
+    fun check source =
+     (Resources.check_file ctxt (SOME base_dir) source;
+      Path.explode (Input.string_of source));
+    val files = map check raw_files;
+  in (files, base_dir) end;
+
+fun get_external_files dir (files, base_dir) =
+  files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir);
+
+
 (* compile_generated_files *)
 
 val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
@@ -287,9 +305,7 @@
       val files = maps get_files_in args;
       val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
       val _ = List.app (write_file dir o #1) files;
-      val _ =
-        external |> List.app (fn (files, base_dir) =>
-          files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
+      val _ = List.app (get_external_files dir) external;
       val _ =
         ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
           ML_Compiler.flags (Input.pos_of source)
@@ -320,14 +336,7 @@
 fun compile_generated_files_cmd ctxt args external export export_prefix source =
   compile_generated_files ctxt
     (map (check_files_in ctxt) args)
-    (external |> map (fn (raw_files, raw_base_dir) =>
-      let
-        val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
-        fun check source =
-         (Resources.check_file ctxt (SOME base_dir) source;
-          Path.explode (Input.string_of source));
-        val files = map check raw_files;
-      in (files, base_dir) end))
+    (map (check_external_files ctxt) external)
     ((map o apfst o map) Path.explode_binding export)
     (Path.explode_binding export_prefix)
     source;