diff -r efd169aed4dc -r 2c7cfd2f9b6c src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Jul 16 11:43:32 2020 +0200 +++ b/src/Pure/PIDE/resources.ML Thu Jul 16 14:36:43 2020 +0200 @@ -121,8 +121,10 @@ ( type T = files; val empty = make_files (Path.current, [], []); - fun extend _ = empty; - fun merge _ = empty; + val extend = I; + fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = + let val provided' = Library.merge (op =) (provided1, provided2) + in make_files (master_dir, imports, provided') end ); fun map_files f =