src/Pure/Tools/generated_files.ML
changeset 69662 fd86ed39aea4
parent 69628 a2fbfdc5e62d
child 69784 24bbc4e30e5b
     1.1 --- a/src/Pure/Tools/generated_files.ML	Mon Jan 14 18:35:03 2019 +0000
     1.2 +++ b/src/Pure/Tools/generated_files.ML	Tue Jan 15 20:03:53 2019 +0100
     1.3 @@ -7,9 +7,9 @@
     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.T * string) list
     1.8 -  val write_files: theory -> Path.T -> Path.T list
     1.9 -  val export_files: theory -> Path.T list
    1.10 +  val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
    1.11 +  val write_files: theory -> Path.T -> (Path.T * Position.T) list
    1.12 +  val export_files: theory -> theory list -> (Path.T * Position.T) list
    1.13    type file_type =
    1.14      {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
    1.15    val file_type:
    1.16 @@ -67,18 +67,21 @@
    1.17        | NONE => (path, (pos, text)) :: files))
    1.18    end;
    1.19  
    1.20 -val get_files = map (apsnd #2) o rev o #1 o Data.get;
    1.21 +val get_files =
    1.22 +  map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
    1.23  
    1.24  fun write_files thy dir =
    1.25 -  get_files thy |> map (fn (path, text) =>
    1.26 +  get_files thy |> map (fn {path, pos, text} =>
    1.27      let
    1.28        val path' = Path.expand (Path.append dir path);
    1.29        val _ = Isabelle_System.mkdirs (Path.dir path');
    1.30        val _ = File.generate path' text;
    1.31 -    in path end);
    1.32 +    in (path, pos) end);
    1.33  
    1.34 -fun export_files thy =
    1.35 -  get_files thy |> map (fn (path, text) => (Export.export thy (Path.implode path) [text]; path));
    1.36 +fun export_files thy other_thys =
    1.37 +  other_thys |> maps (fn other_thy =>
    1.38 +    get_files other_thy |> map (fn {path, pos, text} =>
    1.39 +      (Export.export thy (Path.implode path) [text]; (path, pos))));
    1.40  
    1.41  
    1.42  (* file types *)