src/Pure/Tools/generated_files.ML
changeset 70012 36aeb535a801
parent 69784 24bbc4e30e5b
child 70013 6de8b7a5cd44
     1.1 --- a/src/Pure/Tools/generated_files.ML	Fri Mar 29 13:42:17 2019 +0100
     1.2 +++ b/src/Pure/Tools/generated_files.ML	Fri Mar 29 13:48:10 2019 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature GENERATED_FILES =
     1.5  sig
     1.6    val add_files: (Path.T * Position.T) * string -> theory -> theory
     1.7 -  val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
     1.8 +  val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
     1.9    val write_files: theory -> Path.T -> (Path.T * Position.T) list
    1.10    val export_files: theory -> theory list -> (Path.T * Position.T) list
    1.11    type file_type =
    1.12 @@ -52,7 +52,7 @@
    1.13  
    1.14  (* files *)
    1.15  
    1.16 -fun add_files ((path0, pos), text) =
    1.17 +fun add_files ((path0, pos), content) =
    1.18    let
    1.19      val path = Path.expand path0;
    1.20      fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps);
    1.21 @@ -64,24 +64,25 @@
    1.22      (Data.map o @{apply 3(1)}) (fn files =>
    1.23        (case AList.lookup (op =) files path of
    1.24          SOME (pos', _) => err "Duplicate generated file" [pos, pos']
    1.25 -      | NONE => (path, (pos, text)) :: files))
    1.26 +      | NONE => (path, (pos, content)) :: files))
    1.27    end;
    1.28  
    1.29  val get_files =
    1.30 -  map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
    1.31 +  map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}) o
    1.32 +    rev o #1 o Data.get;
    1.33  
    1.34  fun write_files thy dir =
    1.35 -  get_files thy |> map (fn {path, pos, text} =>
    1.36 +  get_files thy |> map (fn {path, pos, content} =>
    1.37      let
    1.38        val path' = Path.expand (Path.append dir path);
    1.39        val _ = Isabelle_System.mkdirs (Path.dir path');
    1.40 -      val _ = File.generate path' text;
    1.41 +      val _ = File.generate path' content;
    1.42      in (path, pos) end);
    1.43  
    1.44  fun export_files thy other_thys =
    1.45    other_thys |> maps (fn other_thy =>
    1.46 -    get_files other_thy |> map (fn {path, pos, text} =>
    1.47 -      (Export.export thy path [text]; (path, pos))));
    1.48 +    get_files other_thy |> map (fn {path, pos, content} =>
    1.49 +      (Export.export thy path [content]; (path, pos))));
    1.50  
    1.51  
    1.52  (* file types *)
    1.53 @@ -171,8 +172,8 @@
    1.54          handle ERROR msg => error (msg ^ Position.here pos);
    1.55  
    1.56      val header = #make_comment file_type " generated by Isabelle ";
    1.57 -    val text = header ^ "\n" ^ read_source lthy file_type source;
    1.58 -  in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), text) end;
    1.59 +    val content = header ^ "\n" ^ read_source lthy file_type source;
    1.60 +  in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), content) end;
    1.61  
    1.62   
    1.63