equal
deleted
inserted
replaced
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))); |