# HG changeset patch # User wenzelm # Date 1594908052 -7200 # Node ID c386d1b77762c5d3fae2dca60e45ea8c0e1060b9 # Parent 2c7cfd2f9b6c9bdf079df974c69519afb4094083 more thorough extend/merge (for Theory.join_theory); diff -r 2c7cfd2f9b6c -r c386d1b77762 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Thu Jul 16 14:36:43 2020 +0200 +++ b/src/Pure/Tools/generated_files.ML Thu Jul 16 16:00:52 2020 +0200 @@ -57,6 +57,9 @@ type antiquotation = Token.src -> Proof.context -> file_type -> string; +fun err_dup_files path pos pos' = + error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']); + structure Data = Theory_Data ( type T = @@ -67,11 +70,17 @@ ([], Name_Space.empty_table Markup.file_typeN, Name_Space.empty_table Markup.antiquotationN); - val extend = @{apply 3(1)} (K []); - fun merge ((_, types1, antiqs1), (_, types2, antiqs2)) = - ([], - Name_Space.merge_tables (types1, types2), - Name_Space.merge_tables (antiqs1, antiqs2)); + val extend = I; + fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) = + let + val files' = (files1, files2) + |> Library.merge (fn ((path1, file1), (path2, file2)) => + if path1 <> path2 then false + else if file1 = file2 then true + else err_dup_files path1 (#1 file1) (#1 file2)); + val types' = Name_Space.merge_tables (types1, types2); + val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2); + in (files', types', antiqs') end; ); fun add_files (binding, content) = @@ -81,11 +90,16 @@ in (Data.map o @{apply 3(1)}) (fn files => (case AList.lookup (op =) files path of - SOME (pos', _) => - error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']) + SOME (pos', _) => err_dup_files path pos pos' | NONE => (path, (pos, content)) :: files)) end; +fun reset_files thy = + if null (#1 (Data.get thy)) then NONE + else SOME (Data.map (@{apply 3(1)} (K [])) thy); + +val _ = Theory.setup (Theory.at_begin reset_files); + (* get files *)