23 struct |
23 struct |
24 |
24 |
25 (* new locales *) |
25 (* new locales *) |
26 |
26 |
27 fun locale_extern new_locale x = |
27 fun locale_extern new_locale x = |
28 if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x; |
28 if new_locale then NewLocale.extern x else Locale.extern x; |
29 fun locale_add_type_syntax new_locale x = |
29 fun locale_add_type_syntax new_locale x = |
30 if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x; |
30 if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x; |
31 fun locale_add_term_syntax new_locale x = |
31 fun locale_add_term_syntax new_locale x = |
32 if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x; |
32 if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x; |
33 fun locale_add_declaration new_locale x = |
33 fun locale_add_declaration new_locale x = |
34 if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x; |
34 if new_locale then NewLocale.add_declaration x else Locale.add_declaration x; |
35 fun locale_add_thmss new_locale x = |
35 fun locale_add_thmss new_locale x = |
36 if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x; |
36 if new_locale then NewLocale.add_thmss x else Locale.add_thmss x; |
37 fun locale_init new_locale x = |
37 fun locale_init new_locale x = |
38 if !new_locales andalso new_locale then NewLocale.init x else Locale.init x; |
38 if new_locale then NewLocale.init x else Locale.init x; |
39 fun locale_intern new_locale x = |
39 fun locale_intern new_locale x = |
40 if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x; |
40 if new_locale then NewLocale.intern x else Locale.intern x; |
41 |
41 |
42 (* context data *) |
42 (* context data *) |
43 |
43 |
44 datatype target = Target of {target: string, new_locale: bool, is_locale: bool, |
44 datatype target = Target of {target: string, new_locale: bool, is_locale: bool, |
45 is_class: bool, instantiation: string list * (string * sort) list * sort, |
45 is_class: bool, instantiation: string list * (string * sort) list * sort, |