190 val name = "Pure/old-locales"; |
190 val name = "Pure/old-locales"; |
191 type T = locale_data; |
191 type T = locale_data; |
192 |
192 |
193 val empty = make_locale_data NameSpace.empty Symtab.empty (ref []); |
193 val empty = make_locale_data NameSpace.empty Symtab.empty (ref []); |
194 fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs); |
194 fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs); |
195 val finish = I; |
|
196 fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []); |
195 fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []); |
197 fun merge ({space = space1, locales = locales1, scope = _}, |
196 fun merge ({space = space1, locales = locales1, scope = _}, |
198 {space = space2, locales = locales2, scope = _}) = |
197 {space = space2, locales = locales2, scope = _}) = |
199 make_locale_data (NameSpace.merge (space1, space2)) |
198 make_locale_data (NameSpace.merge (space1, space2)) |
200 (Symtab.merge (K true) (locales1, locales2)) |
199 (Symtab.merge (K true) (locales1, locales2)) |