# HG changeset patch
# User wenzelm
# Date 1553863690 -3600
# Node ID 36aeb535a801e950deb94ffbbf48504d3318d58e
# Parent  9dde788b0128a2d5ececb93da503e2b4104179f6
tuned signature;

diff -r 9dde788b0128 -r 36aeb535a801 src/Pure/Tools/generated_files.ML
--- 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;