--- a/src/Pure/Tools/generated_files.ML Fri Mar 29 13:42:17 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML Fri Mar 29 13:48:10 2019 +0100
@@ -7,7 +7,7 @@
signature GENERATED_FILES =
sig
val add_files: (Path.T * Position.T) * string -> theory -> theory
- val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
+ 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
type file_type =
@@ -52,7 +52,7 @@
(* files *)
-fun add_files ((path0, pos), text) =
+fun add_files ((path0, pos), content) =
let
val path = Path.expand path0;
fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps);
@@ -64,24 +64,25 @@
(Data.map o @{apply 3(1)}) (fn files =>
(case AList.lookup (op =) files path of
SOME (pos', _) => err "Duplicate generated file" [pos, pos']
- | NONE => (path, (pos, text)) :: files))
+ | NONE => (path, (pos, content)) :: files))
end;
val get_files =
- map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
+ map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}) o
+ rev o #1 o Data.get;
fun write_files thy dir =
- get_files thy |> map (fn {path, pos, text} =>
+ 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' text;
+ val _ = File.generate path' content;
in (path, pos) end);
fun export_files thy other_thys =
other_thys |> maps (fn other_thy =>
- get_files other_thy |> map (fn {path, pos, text} =>
- (Export.export thy path [text]; (path, pos))));
+ get_files other_thy |> map (fn {path, pos, content} =>
+ (Export.export thy path [content]; (path, pos))));
(* file types *)
@@ -171,8 +172,8 @@
handle ERROR msg => error (msg ^ Position.here pos);
val header = #make_comment file_type " generated by Isabelle ";
- val text = header ^ "\n" ^ read_source lthy file_type source;
- in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), text) end;
+ val content = header ^ "\n" ^ read_source lthy file_type source;
+ in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), content) end;