1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Dec 12 15:02:15 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 12 17:00:42 2008 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  signature THEORY_TARGET =
     1.6  sig
     1.7 -  val peek: local_theory -> {target: string, is_locale: bool,
     1.8 +  val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
     1.9      is_class: bool, instantiation: string list * (string * sort) list * sort,
    1.10      overloading: (string * (string * typ) * bool) list}
    1.11    val init: string option -> theory -> local_theory
    1.12 @@ -24,32 +24,32 @@
    1.13  
    1.14  (* new locales *)
    1.15  
    1.16 -fun locale_extern is_class x = 
    1.17 -  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
    1.18 -fun locale_add_type_syntax is_class x =
    1.19 -  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.20 -fun locale_add_term_syntax is_class x =
    1.21 -  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.22 -fun locale_add_declaration is_class x =
    1.23 -  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
    1.24 -fun locale_add_thmss is_class x =
    1.25 -  if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
    1.26 -fun locale_init x =
    1.27 -  if !new_locales then NewLocale.init x else Locale.init x;
    1.28 -fun locale_intern is_class x =
    1.29 -  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
    1.30 +fun locale_extern new_locale x = 
    1.31 +  if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
    1.32 +fun locale_add_type_syntax new_locale x =
    1.33 +  if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.34 +fun locale_add_term_syntax new_locale x =
    1.35 +  if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.36 +fun locale_add_declaration new_locale x =
    1.37 +  if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
    1.38 +fun locale_add_thmss new_locale x =
    1.39 +  if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
    1.40 +fun locale_init new_locale x =
    1.41 +  if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
    1.42 +fun locale_intern new_locale x =
    1.43 +  if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
    1.44  
    1.45  (* context data *)
    1.46  
    1.47 -datatype target = Target of {target: string, is_locale: bool,
    1.48 +datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
    1.49    is_class: bool, instantiation: string list * (string * sort) list * sort,
    1.50    overloading: (string * (string * typ) * bool) list};
    1.51  
    1.52 -fun make_target target is_locale is_class instantiation overloading =
    1.53 -  Target {target = target, is_locale = is_locale,
    1.54 +fun make_target target new_locale is_locale is_class instantiation overloading =
    1.55 +  Target {target = target, new_locale = new_locale, is_locale = is_locale,
    1.56      is_class = is_class, instantiation = instantiation, overloading = overloading};
    1.57  
    1.58 -val global_target = make_target "" false false ([], [], []) [];
    1.59 +val global_target = make_target "" false false false ([], [], []) [];
    1.60  
    1.61  structure Data = ProofDataFun
    1.62  (
    1.63 @@ -80,7 +80,7 @@
    1.64        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
    1.65    end;
    1.66  
    1.67 -fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
    1.68 +fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
    1.69    Pretty.block [Pretty.str "theory", Pretty.brk 1,
    1.70        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    1.71      (if not (null overloading) then [Overloading.pretty ctxt]
    1.72 @@ -90,7 +90,7 @@
    1.73  
    1.74  (* target declarations *)
    1.75  
    1.76 -fun target_decl add (Target {target, is_class, ...}) d lthy =
    1.77 +fun target_decl add (Target {target, new_locale, ...}) d lthy =
    1.78    let
    1.79      val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    1.80      val d0 = Morphism.form d';
    1.81 @@ -101,7 +101,7 @@
    1.82        |> LocalTheory.target (Context.proof_map d0)
    1.83      else
    1.84        lthy
    1.85 -      |> LocalTheory.target (add is_class target d')
    1.86 +      |> LocalTheory.target (add new_locale target d')
    1.87    end;
    1.88  
    1.89  val type_syntax = target_decl locale_add_type_syntax;
    1.90 @@ -167,7 +167,7 @@
    1.91    |> ProofContext.note_thmss_i kind facts
    1.92    ||> ProofContext.restore_naming ctxt;
    1.93  
    1.94 -fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
    1.95 +fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
    1.96    let
    1.97      val thy = ProofContext.theory_of lthy;
    1.98      val facts' = facts
    1.99 @@ -186,7 +186,7 @@
   1.100          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
   1.101          #> Sign.restore_naming thy)
   1.102      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
   1.103 -    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
   1.104 +    |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
   1.105      |> note_local kind local_facts
   1.106    end;
   1.107  
   1.108 @@ -335,13 +335,14 @@
   1.109  
   1.110  fun init_target _ NONE = global_target
   1.111    | init_target thy (SOME target) =
   1.112 -      make_target target true (Class.is_class thy target) ([], [], []) [];
   1.113 +      make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
   1.114 +      true (Class.is_class thy target) ([], [], []) [];
   1.115  
   1.116 -fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   1.117 +fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
   1.118    if not (null (#1 instantiation)) then Class.init_instantiation instantiation
   1.119    else if not (null overloading) then Overloading.init overloading
   1.120    else if not is_locale then ProofContext.init
   1.121 -  else if not is_class then locale_init target
   1.122 +  else if not is_class then locale_init new_locale target
   1.123    else Class.init target;
   1.124  
   1.125  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   1.126 @@ -366,7 +367,7 @@
   1.127      val ctxt = ProofContext.init thy;
   1.128      val ops = raw_ops |> map (fn (name, const, checked) =>
   1.129        (name, Term.dest_Const (prep_const ctxt const), checked));
   1.130 -  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
   1.131 +  in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
   1.132  
   1.133  in
   1.134  
   1.135 @@ -375,9 +376,9 @@
   1.136  
   1.137  fun context "-" thy = init NONE thy
   1.138    | context target thy = init (SOME (locale_intern
   1.139 -      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
   1.140 +      (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
   1.141  
   1.142 -fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
   1.143 +fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
   1.144  
   1.145  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   1.146  val overloading_cmd = gen_overloading Syntax.read_term;