clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
tuned concrete syntax;

--- a/src/Pure/Pure.thy	Thu Apr 04 15:26:18 2019 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 04 16:47:09 2019 +0200
@@ -130,20 +130,24 @@
 
   val files_in =
     (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
-      Scan.option (\<^keyword>\<open>in\<close> |-- Parse.!!! Parse.theory_name);
+      Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
       "export generated files from given theories"
       (Parse.and_list1 files_in >> (fn args =>
         Toplevel.keep (fn st =>
-          Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)))
+          Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)));
+
 
+  val base_dir =
+    Scan.optional (\<^keyword>\<open>(\<close> |--
+      Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.position Parse.path --| \<^keyword>\<open>)\<close>)) ("", Position.none);
+
+  val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir;
 
   val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false;
-
-  val executable =
-    \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
+  val executable = \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
 
   val export_files = Scan.repeat1 Parse.path_binding -- executable;
 
@@ -151,8 +155,7 @@
     Outer_Syntax.command \<^command_keyword>\<open>compile_generated_files\<close>
       "compile generated files and export results"
       (Parse.and_list files_in --
-        Scan.optional (\<^keyword>\<open>external_files\<close> |--
-          Parse.!!! (Scan.repeat1 (Parse.position Parse.path))) [] --
+        Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
         Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
         Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("compiled", Position.none) --
         (Parse.where_ |-- Parse.!!! Parse.ML_source)

--- a/src/Pure/Tools/generated_files.ML	Thu Apr 04 15:26:18 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Apr 04 16:47:09 2019 +0200
@@ -34,11 +34,15 @@
   val export_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list -> unit
   val with_compile_dir: (Path.T -> unit) -> unit
-  val compile_generated_files: Proof.context -> (Path.binding list * theory) list ->
-    Path.T list -> (Path.binding list * bool option) list -> Path.binding -> Input.source -> unit
+  val compile_generated_files: Proof.context ->
+    (Path.binding list * theory) list ->
+    (Path.T list * Path.T) list ->
+    (Path.binding list * bool option) list ->
+    Path.binding -> Input.source -> unit
   val compile_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list ->
-    (string * Position.T) list -> ((string * Position.T) list * bool option) list ->
+    ((string * Position.T) list * (string * Position.T)) list ->
+    ((string * Position.T) list * bool option) list ->
     string * Position.T -> Input.source -> unit
 end;
 
@@ -259,7 +263,9 @@
       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 file => Isabelle_System.copy_file file dir);
+      val _ =
+        external |> List.app (fn (files, base_dir) =>
+          files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
       val _ =
         ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
           ML_Compiler.flags (Input.pos_of source)
@@ -290,7 +296,12 @@
 fun compile_generated_files_cmd ctxt args external export export_prefix source =
   compile_generated_files ctxt
     (map (check_files_in ctxt) args)
-    (map (Resources.check_file ctxt NONE) external)
+    (external |> map (fn (raw_files, raw_base_dir) =>
+      let
+        val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
+        fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s);
+        val files = map check raw_files;
+      in (files, base_dir) end))
     ((map o apfst o map) Path.explode_binding export)
     (Path.explode_binding export_prefix)
     source;