--- 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 *)