src/Pure/PIDE/resources.ML
changeset 72045 2c7cfd2f9b6c
parent 71912 b9fbc93f3a24
child 72103 7b318273a4aa
equal deleted inserted replaced
72044:efd169aed4dc 72045:2c7cfd2f9b6c
   119 
   119 
   120 structure Files = Theory_Data
   120 structure Files = Theory_Data
   121 (
   121 (
   122   type T = files;
   122   type T = files;
   123   val empty = make_files (Path.current, [], []);
   123   val empty = make_files (Path.current, [], []);
   124   fun extend _ = empty;
   124   val extend = I;
   125   fun merge _ = empty;
   125   fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
       
   126     let val provided' = Library.merge (op =) (provided1, provided2)
       
   127     in make_files (master_dir, imports, provided') end
   126 );
   128 );
   127 
   129 
   128 fun map_files f =
   130 fun map_files f =
   129   Files.map (fn {master_dir, imports, provided} =>
   131   Files.map (fn {master_dir, imports, provided} =>
   130     make_files (f (master_dir, imports, provided)));
   132     make_files (f (master_dir, imports, provided)));