clarified signature: more explicit operations for corresponding Isar commands;

--- a/src/Pure/Isar/parse.ML	Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Apr 03 21:50:00 2019 +0200
@@ -70,6 +70,7 @@
   val embedded_position: (string * Position.T) parser
   val text: string parser
   val path: string parser
+  val path_binding: (string * Position.T) parser
   val session_name: (string * Position.T) parser
   val theory_name: (string * Position.T) parser
   val liberal_name: string parser
@@ -282,6 +283,7 @@
 val text = group (fn () => "text") (embedded || verbatim);
 
 val path = group (fn () => "file name/path specification") embedded;
+val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
 
 val session_name = group (fn () => "session name") name_position;
 val theory_name = group (fn () => "theory name") name_position;

--- a/src/Pure/Pure.thy	Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Pure/Pure.thy	Wed Apr 03 21:50:00 2019 +0200
@@ -123,29 +123,20 @@
   val _ =
     Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
       "generate source file, with antiquotations"
-      (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+      (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
         >> Generated_Files.generate_file_cmd);
 
+  val files_in =
+    (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
+      Scan.option (\<^keyword>\<open>in\<close> |-- Parse.!!! Parse.theory_name);
+
   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 =>
+      "export generated files from given theories"
+      (Parse.and_list1 files_in >> (fn args =>
         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 Path.current);
-               writeln (cat_lines (paths |> map (fn (path, pos) =>
-                Markup.markup (Markup.entityN, Position.def_properties_of pos)
-                  (quote (Path.implode path))))))
-            else ()
-          end)));
+          Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)))
+
 in end\<close>
 
 

--- a/src/Pure/Tools/generated_files.ML	Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Wed Apr 03 21:50:00 2019 +0200
@@ -7,10 +7,16 @@
 signature GENERATED_FILES =
 sig
   val add_files: Path.binding * string -> theory -> theory
-  val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
-  val write_files: theory -> Path.T -> (Path.T * Position.T) list
-  val export_files: theory -> theory list -> (Path.T * Position.T) list
-  val the_file_content: theory -> Path.T -> string
+  type file = {path: Path.T, pos: Position.T, content: string}
+  val file_binding: file -> Path.binding
+  val print_file: file -> string
+  val get_files: theory -> file list
+  val get_file: theory -> Path.binding -> file
+  val get_files_in: Path.binding list * theory -> file list
+  val check_files_in: Proof.context ->
+    (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
+  val write_file: Path.T -> file -> unit
+  val export_file: theory -> file -> unit
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
@@ -20,7 +26,11 @@
     ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
     theory -> theory
   val set_string: string -> Proof.context -> Proof.context
+  val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
   val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
+  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
 end;
 
 structure Generated_Files: GENERATED_FILES =
@@ -50,9 +60,6 @@
      Name_Space.merge_tables (antiqs1, antiqs2));
 );
 
-
-(* files *)
-
 fun add_files (binding, content) =
   let val (path, pos) = Path.dest_binding binding in
     (Data.map o @{apply 3(1)}) (fn files =>
@@ -62,34 +69,58 @@
       | NONE => (path, (pos, content)) :: files))
   end;
 
-val get_files =
-  map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}) o
-    rev o #1 o Data.get;
+
+(* get files *)
+
+type file = {path: Path.T, pos: Position.T, content: string};
+
+fun file_binding (file: file) = Path.binding (#path file, #pos file);
+
+fun print_file (file: file) =
+  quote (Path.implode (#path file))
+  |> Markup.markup (Markup.entityN, Position.def_properties_of (#pos file));
 
-fun write_files thy dir =
-  get_files thy |> map (fn {path, pos, content} =>
-    let
-      val path' = Path.expand (Path.append dir path);
-      val _ = Isabelle_System.mkdirs (Path.dir path');
-      val _ = File.generate path' content;
-    in (path, pos) end);
+fun get_files thy =
+  Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
+    {path = path, pos = pos, content = content}: file);
+
+fun get_file thy binding =
+  let val (path, pos) = Path.dest_binding binding in
+    (case find_first (fn file => #path file = path) (get_files thy) of
+      SOME file => file
+    | NONE =>
+        error ("Missing generated file " ^ Path.print path ^
+          " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
+  end;
 
-fun export_files thy other_thys =
-  other_thys |> maps (fn other_thy =>
-    get_files other_thy |> map (fn {path, pos, content} =>
-      (Export.export thy (Path.binding (path, pos)) [content]; (path, pos))));
+fun get_files_in ([], thy) = get_files thy
+  | get_files_in (files, thy) = map (get_file thy) files;
+
+
+(* check and output files *)
 
-fun the_file_content thy path =
-  (case find_first (fn file => #path file = path) (get_files thy) of
-    SOME {content, ...} => content
-  | NONE =>
-      error ("Missing generated file " ^ Path.print path ^
-        " in theory " ^ quote (Context.theory_long_name thy)));
+fun check_files_in ctxt (files, opt_thy) =
+  let
+    val thy =
+      (case opt_thy of
+        SOME name => Theory.check {long = false} ctxt name
+      | NONE => Proof_Context.theory_of ctxt);
+  in (map Path.explode_binding files, thy) end;
+
+fun write_file dir (file: file) =
+  let
+    val path = Path.expand (Path.append dir (#path file));
+    val _ = Isabelle_System.mkdirs (Path.dir path);
+    val _ = File.generate path (#content file);
+  in () end;
+
+fun export_file thy (file: file) =
+  Export.export thy (file_binding file) [#content file];
 
 
 (* file types *)
 
-fun the_file_type thy ext =
+fun get_file_type thy ext =
   if ext = "" then error "Bad file extension"
   else
     (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
@@ -110,7 +141,7 @@
     val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
 
     val _ =
-      (case try (#name o the_file_type thy) ext of
+      (case try (#name o get_file_type thy) ext of
         NONE => ()
       | SOME name' =>
           error ("Extension " ^ quote ext ^ " already registered for file type " ^
@@ -162,24 +193,40 @@
   in implode (map expand input) end;
 
 
-(* generate files *)
 
-fun generate_file_cmd ((file, pos), source) lthy =
+(** Isar commands **)
+
+fun generate_file (binding, source) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
-    val path = Path.explode file;
-    val binding = Path.binding (path, pos);
+    val (path, pos) = Path.dest_binding binding;
     val file_type =
-      the_file_type thy (#2 (Path.split_ext path))
+      get_file_type thy (#2 (Path.split_ext path))
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
     val content = header ^ "\n" ^ read_source lthy file_type source;
   in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
 
+fun generate_file_cmd (file, source) lthy =
+  generate_file (Path.explode_binding file, source) lthy;
+
+fun export_generated_files ctxt args =
+  let val thy = Proof_Context.theory_of ctxt in
+    (case maps get_files_in args of
+      [] => ()
+    | files =>
+       (List.app (export_file thy) files;
+        writeln (Export.message thy Path.current);
+        writeln (cat_lines (map (prefix "  " o print_file) files))))
+  end;
+
+fun export_generated_files_cmd ctxt args =
+  export_generated_files ctxt (map (check_files_in ctxt) args);
  
 
+
 (** concrete file types **)
 
 val _ =

--- a/src/Tools/Haskell/Haskell.thy	Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed Apr 03 21:50:00 2019 +0200
@@ -1943,6 +1943,6 @@
       return ()
 \<close>
 
-export_generated_files
+export_generated_files _
 
 end

--- a/src/Tools/Haskell/Test.thy	Wed Apr 03 21:11:21 2019 +0200
+++ b/src/Tools/Haskell/Test.thy	Wed Apr 03 21:50:00 2019 +0200
@@ -11,10 +11,11 @@
   Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
     let
       val src_dir = Path.append tmp_dir (Path.explode "src");
-      val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
+      val files = Generated_Files.get_files \<^theory>\<open>Haskell\<close>;
+      val _ = List.app (Generated_Files.write_file src_dir) files;
 
       val modules = files
-        |> map (#1 #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
+        |> map (#path #> Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
       val _ =
         GHC.new_project tmp_dir
           {name = "isabelle",