# HG changeset patch
# User wenzelm
# Date 1553874826 -3600
# Node ID 6de8b7a5cd4429a10dc4c4035f62383aa71a47c4
# Parent  36aeb535a801e950deb94ffbbf48504d3318d58e
tuned signature -- more operations;

diff -r 36aeb535a801 -r 6de8b7a5cd44 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Mar 29 13:48:10 2019 +0100
+++ b/src/Pure/General/path.ML	Fri Mar 29 16:53:46 2019 +0100
@@ -33,6 +33,7 @@
   val base: T -> T
   val ext: string -> T -> T
   val split_ext: T -> T * string
+  val exe: T -> T
   val expand: T -> T
   val file_name: T -> string
   val smart_implode: T -> string
@@ -202,6 +203,8 @@
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
+val exe = ML_System.platform_is_windows ? ext "exe";
+
 
 (* expand variables *)
 
diff -r 36aeb535a801 -r 6de8b7a5cd44 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Fri Mar 29 13:48:10 2019 +0100
+++ b/src/Pure/Thy/export.ML	Fri Mar 29 16:53:46 2019 +0100
@@ -11,6 +11,8 @@
   val export_params: params -> string list -> unit
   val export: theory -> Path.T -> string list -> unit
   val export_executable: theory -> Path.T -> string list -> unit
+  val export_file: theory -> Path.T -> Path.T -> unit
+  val export_executable_file: theory -> Path.T -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
 end;
@@ -39,11 +41,14 @@
     executable = executable,
     compress = compress} blob;
 
-fun export theory path blob =
-  export_params {theory = theory, path = path, executable = false, compress = true} blob;
+fun export thy path blob =
+  export_params {theory = thy, path = path, executable = false, compress = true} blob;
 
-fun export_executable theory path blob =
-  export_params {theory = theory, path = path, executable = true, compress = true} blob;
+fun export_executable thy path blob =
+  export_params {theory = thy, path = path, executable = true, compress = true} blob;
+
+fun export_file thy path file = export thy path [File.read file];
+fun export_executable_file thy path file = export_executable thy path [File.read file];
 
 
 (* information message *)
diff -r 36aeb535a801 -r 6de8b7a5cd44 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Mar 29 13:48:10 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Mar 29 16:53:46 2019 +0100
@@ -10,6 +10,7 @@
   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_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
@@ -84,6 +85,13 @@
     get_files other_thy |> map (fn {path, pos, content} =>
       (Export.export thy path [content]; (path, pos))));
 
+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)));
+
 
 (* file types *)