Code for switching to new locales.
authorballarin
Tue Nov 18 09:41:23 2008 +0100 (2008-11-18)
changeset 2883466d31ca2c5af
parent 28833 f356687a7659
child 28835 d4d8eba5f781
Code for switching to new locales.
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Nov 18 09:40:44 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Nov 18 09:41:23 2008 +0100
     1.3 @@ -21,6 +21,18 @@
     1.4  structure TheoryTarget: THEORY_TARGET =
     1.5  struct
     1.6  
     1.7 +(* new locales *)
     1.8 +
     1.9 +val new_locales = false;
    1.10 +
    1.11 +fun locale_extern x = if new_locales then NewLocale.extern x else Locale.extern x;
    1.12 +fun locale_add_type_syntax x = if new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.13 +fun locale_add_term_syntax x = if new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.14 +fun locale_add_declaration x = if new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    1.15 +fun locale_add_thmss x = if new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    1.16 +fun locale_init x = if new_locales then NewLocale.init x else Locale.init x;
    1.17 +fun locale_intern x = if new_locales then NewLocale.intern x else Locale.intern x;
    1.18 +
    1.19  (* context data *)
    1.20  
    1.21  datatype target = Target of {target: string, is_locale: bool,
    1.22 @@ -47,7 +59,7 @@
    1.23  fun pretty_thy ctxt target is_locale is_class =
    1.24    let
    1.25      val thy = ProofContext.theory_of ctxt;
    1.26 -    val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.27 +    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
    1.28      val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
    1.29        (#1 (ProofContext.inferred_fixes ctxt));
    1.30      val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
    1.31 @@ -86,9 +98,9 @@
    1.32        |> LocalTheory.target (add target d')
    1.33    end;
    1.34  
    1.35 -val type_syntax = target_decl Locale.add_type_syntax;
    1.36 -val term_syntax = target_decl Locale.add_term_syntax;
    1.37 -val declaration = target_decl Locale.add_declaration;
    1.38 +val type_syntax = target_decl locale_add_type_syntax;
    1.39 +val term_syntax = target_decl locale_add_term_syntax;
    1.40 +val declaration = target_decl locale_add_declaration;
    1.41  
    1.42  fun class_target (Target {target, ...}) f =
    1.43    LocalTheory.raw_theory f #>
    1.44 @@ -170,7 +182,7 @@
    1.45          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    1.46          #> Sign.restore_naming thy)
    1.47      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.48 -    |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    1.49 +    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
    1.50      |> note_local kind local_facts
    1.51    end;
    1.52  
    1.53 @@ -325,7 +337,7 @@
    1.54    if not (null (#1 instantiation)) then Class.init_instantiation instantiation
    1.55    else if not (null overloading) then Overloading.init overloading
    1.56    else if not is_locale then ProofContext.init
    1.57 -  else if not is_class then Locale.init target
    1.58 +  else if not is_class then locale_init target
    1.59    else Class.init target;
    1.60  
    1.61  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
    1.62 @@ -358,7 +370,7 @@
    1.63  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
    1.64  
    1.65  fun context "-" thy = init NONE thy
    1.66 -  | context target thy = init (SOME (Locale.intern thy target)) thy;
    1.67 +  | context target thy = init (SOME (locale_intern thy target)) thy;
    1.68  
    1.69  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    1.70