renamed Theory_Target to the more appropriate Named_Target
authorhaftmann
Wed Aug 11 14:45:38 2010 +0200 (2010-08-11 ago)
changeset 38350480b2de9927c
parent 38349 ed50e21e715a
child 38351 ea1ee55aa41f
child 38375 43a765bc7ff0
child 38430 254a021ed66e
renamed Theory_Target to the more appropriate Named_Target
src/HOL/Statespace/state_space.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/typedef.ML
src/Pure/IsaMakefile
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Isar/toplevel.ML
src/Pure/Isar/typedecl.ML
src/Pure/ROOT.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Wed Aug 11 14:41:16 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Aug 11 14:45:38 2010 +0200
     1.3 @@ -348,7 +348,7 @@
     1.4  
     1.5  fun add_declaration name decl thy =
     1.6    thy
     1.7 -  |> Theory_Target.init name
     1.8 +  |> Named_Target.init name
     1.9    |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
    1.10    |> Local_Theory.exit_global;
    1.11  
     2.1 --- a/src/HOL/Tools/inductive.ML	Wed Aug 11 14:41:16 2010 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Aug 11 14:45:38 2010 +0200
     2.3 @@ -998,7 +998,7 @@
     2.4    let
     2.5      val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     2.6      val ctxt' = thy
     2.7 -      |> Theory_Target.init NONE
     2.8 +      |> Named_Target.init NONE
     2.9        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
    2.10        |> Local_Theory.exit;
    2.11      val info = #2 (the_inductive ctxt' name);
     3.1 --- a/src/HOL/Tools/primrec.ML	Wed Aug 11 14:41:16 2010 +0200
     3.2 +++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 14:45:38 2010 +0200
     3.3 @@ -292,7 +292,7 @@
     3.4  
     3.5  fun add_primrec_global fixes specs thy =
     3.6    let
     3.7 -    val lthy = Theory_Target.init NONE thy;
     3.8 +    val lthy = Named_Target.init NONE thy;
     3.9      val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    3.10      val simps' = ProofContext.export lthy' lthy simps;
    3.11    in ((ts, simps'), Local_Theory.exit_global lthy') end;
     4.1 --- a/src/HOL/Tools/typedef.ML	Wed Aug 11 14:41:16 2010 +0200
     4.2 +++ b/src/HOL/Tools/typedef.ML	Wed Aug 11 14:45:38 2010 +0200
     4.3 @@ -268,7 +268,7 @@
     4.4    in typedef_result inhabited lthy' end;
     4.5  
     4.6  fun add_typedef_global def opt_name typ set opt_morphs tac =
     4.7 -  Theory_Target.init NONE
     4.8 +  Named_Target.init NONE
     4.9    #> add_typedef def opt_name typ set opt_morphs tac
    4.10    #> Local_Theory.exit_result_global (apsnd o transform_info);
    4.11  
     5.1 --- a/src/Pure/IsaMakefile	Wed Aug 11 14:41:16 2010 +0200
     5.2 +++ b/src/Pure/IsaMakefile	Wed Aug 11 14:45:38 2010 +0200
     5.3 @@ -127,6 +127,7 @@
     5.4    Isar/local_theory.ML					\
     5.5    Isar/locale.ML					\
     5.6    Isar/method.ML					\
     5.7 +  Isar/named_target.ML					\
     5.8    Isar/object_logic.ML					\
     5.9    Isar/obtain.ML					\
    5.10    Isar/outer_syntax.ML					\
    5.11 @@ -144,7 +145,6 @@
    5.12    Isar/skip_proof.ML					\
    5.13    Isar/spec_rules.ML					\
    5.14    Isar/specification.ML					\
    5.15 -  Isar/theory_target.ML					\
    5.16    Isar/token.ML						\
    5.17    Isar/toplevel.ML					\
    5.18    Isar/typedecl.ML					\
     6.1 --- a/src/Pure/Isar/class.ML	Wed Aug 11 14:41:16 2010 +0200
     6.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 11 14:45:38 2010 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  signature CLASS =
     6.5  sig
     6.6    include CLASS_TARGET
     6.7 -    (*FIXME the split into class_target.ML, theory_target.ML and
     6.8 +    (*FIXME the split into class_target.ML, Named_Target.ML and
     6.9        class.ML is artificial*)
    6.10  
    6.11    val class: binding -> class list -> Element.context_i list
    6.12 @@ -296,7 +296,7 @@
    6.13         Context.theory_map (Locale.add_registration (class, base_morph)
    6.14           (Option.map (rpair true) eq_morph) export_morph)
    6.15      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    6.16 -    |> Theory_Target.init (SOME class)
    6.17 +    |> Named_Target.init (SOME class)
    6.18      |> pair class
    6.19    end;
    6.20  
    6.21 @@ -316,7 +316,7 @@
    6.22    let
    6.23      val thy = ProofContext.theory_of lthy;
    6.24      val proto_sup = prep_class thy raw_sup;
    6.25 -    val proto_sub = case Theory_Target.peek lthy
    6.26 +    val proto_sub = case Named_Target.peek lthy
    6.27       of {is_class = false, ...} => error "Not in a class context"
    6.28        | {target, ...} => target;
    6.29      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    6.30 @@ -329,7 +329,7 @@
    6.31      fun after_qed some_wit =
    6.32        ProofContext.theory (register_subclass (sub, sup)
    6.33          some_dep_morph some_wit export)
    6.34 -      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
    6.35 +      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
    6.36    in do_proof after_qed some_prop goal_ctxt end;
    6.37  
    6.38  fun user_proof after_qed some_prop =
     7.1 --- a/src/Pure/Isar/expression.ML	Wed Aug 11 14:41:16 2010 +0200
     7.2 +++ b/src/Pure/Isar/expression.ML	Wed Aug 11 14:45:38 2010 +0200
     7.3 @@ -775,7 +775,7 @@
     7.4      val loc_ctxt = thy'
     7.5        |> Locale.register_locale binding (extraTs, params)
     7.6            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
     7.7 -      |> Theory_Target.init (SOME name)
     7.8 +      |> Named_Target.init (SOME name)
     7.9        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    7.10  
    7.11    in (name, loc_ctxt) end;
    7.12 @@ -870,7 +870,7 @@
    7.13  fun gen_sublocale prep_expr intern raw_target expression thy =
    7.14    let
    7.15      val target = intern thy raw_target;
    7.16 -    val target_ctxt = Theory_Target.init (SOME target) thy;
    7.17 +    val target_ctxt = Named_Target.init (SOME target) thy;
    7.18      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    7.19      fun after_qed witss = ProofContext.theory
    7.20        (fold (fn ((dep, morph), wits) => Locale.add_dependency
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:41:16 2010 +0200
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:45:38 2010 +0200
     8.3 @@ -406,7 +406,7 @@
     8.4  val _ =
     8.5    Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
     8.6      (Parse.name --| Parse.begin >> (fn name =>
     8.7 -      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
     8.8 +      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
     8.9  
    8.10  
    8.11  (* locales *)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 14:45:38 2010 +0200
     9.3 @@ -0,0 +1,211 @@
     9.4 +(*  Title:      Pure/Isar/theory_target.ML
     9.5 +    Author:     Makarius
     9.6 +    Author:     Florian Haftmann, TU Muenchen
     9.7 +
     9.8 +Targets for theory, locale and class.
     9.9 +*)
    9.10 +
    9.11 +signature NAMED_TARGET =
    9.12 +sig
    9.13 +  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
    9.14 +  val init: string option -> theory -> local_theory
    9.15 +  val context_cmd: xstring -> theory -> local_theory
    9.16 +end;
    9.17 +
    9.18 +structure Named_Target: NAMED_TARGET =
    9.19 +struct
    9.20 +
    9.21 +(* context data *)
    9.22 +
    9.23 +datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    9.24 +
    9.25 +fun make_target target is_locale is_class =
    9.26 +  Target {target = target, is_locale = is_locale, is_class = is_class};
    9.27 +
    9.28 +val global_target = make_target "" false false;
    9.29 +
    9.30 +structure Data = Proof_Data
    9.31 +(
    9.32 +  type T = target;
    9.33 +  fun init _ = global_target;
    9.34 +);
    9.35 +
    9.36 +val peek = (fn Target args => args) o Data.get;
    9.37 +
    9.38 +
    9.39 +(* generic declarations *)
    9.40 +
    9.41 +fun locale_declaration locale { syntax, pervasive } decl lthy =
    9.42 +  let
    9.43 +    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    9.44 +    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    9.45 +  in
    9.46 +    lthy
    9.47 +    |> pervasive ? Generic_Target.theory_declaration decl
    9.48 +    |> Local_Theory.target (add locale locale_decl)
    9.49 +  end;
    9.50 +
    9.51 +fun target_declaration (Target {target, ...}) { syntax, pervasive } =
    9.52 +  if target = "" then Generic_Target.theory_declaration
    9.53 +  else locale_declaration target { syntax = syntax, pervasive = pervasive };
    9.54 +
    9.55 +
    9.56 +(* consts in locales *)
    9.57 +
    9.58 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
    9.59 +  let
    9.60 +    val b' = Morphism.binding phi b;
    9.61 +    val rhs' = Morphism.term phi rhs;
    9.62 +    val arg = (b', Term.close_schematic_term rhs');
    9.63 +    val same_shape = Term.aconv_untyped (rhs, rhs');
    9.64 +    (* FIXME workaround based on educated guess *)
    9.65 +    val prefix' = Binding.prefix_of b';
    9.66 +    val is_canonical_class = is_class andalso
    9.67 +      (Binding.eq_name (b, b')
    9.68 +        andalso not (null prefix')
    9.69 +        andalso List.last prefix' = (Class_Target.class_prefix target, false)
    9.70 +      orelse same_shape);
    9.71 +  in
    9.72 +    not is_canonical_class ?
    9.73 +      (Context.mapping_result
    9.74 +        (Sign.add_abbrev Print_Mode.internal arg)
    9.75 +        (ProofContext.add_abbrev Print_Mode.internal arg)
    9.76 +      #-> (fn (lhs' as Const (d, _), _) =>
    9.77 +          same_shape ?
    9.78 +            (Context.mapping
    9.79 +              (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    9.80 +             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    9.81 +  end;
    9.82 +
    9.83 +fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    9.84 +  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
    9.85 +
    9.86 +fun class_target (Target {target, ...}) f =
    9.87 +  Local_Theory.raw_theory f #>
    9.88 +  Local_Theory.target (Class_Target.refresh_syntax target);
    9.89 +
    9.90 +
    9.91 +(* define *)
    9.92 +
    9.93 +fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    9.94 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    9.95 +  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
    9.96 +    #> pair (lhs, def))
    9.97 +
    9.98 +fun class_foundation (ta as Target {target, ...})
    9.99 +    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   9.100 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   9.101 +  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
   9.102 +    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
   9.103 +    #> pair (lhs, def))
   9.104 +
   9.105 +fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
   9.106 +  if is_class then class_foundation ta
   9.107 +  else if is_locale then locale_foundation ta
   9.108 +  else Generic_Target.theory_foundation;
   9.109 +
   9.110 +
   9.111 +(* notes *)
   9.112 +
   9.113 +fun locale_notes locale kind global_facts local_facts lthy = 
   9.114 +  let
   9.115 +    val global_facts' = Attrib.map_facts (K I) global_facts;
   9.116 +    val local_facts' = Element.facts_map
   9.117 +      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
   9.118 +  in
   9.119 +    lthy
   9.120 +    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
   9.121 +    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
   9.122 +  end
   9.123 +
   9.124 +fun target_notes (ta as Target {target, is_locale, ...}) =
   9.125 +  if is_locale then locale_notes target
   9.126 +    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
   9.127 +
   9.128 +
   9.129 +(* abbrev *)
   9.130 +
   9.131 +fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
   9.132 +  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   9.133 +    (fn (lhs, _) => locale_const_declaration ta prmode
   9.134 +      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
   9.135 +
   9.136 +fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
   9.137 +    prmode (b, mx) (global_rhs, t') xs lthy =
   9.138 +  if is_locale
   9.139 +    then lthy
   9.140 +      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
   9.141 +      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
   9.142 +    else lthy
   9.143 +      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
   9.144 +
   9.145 +
   9.146 +(* pretty *)
   9.147 +
   9.148 +fun pretty_thy ctxt target is_class =
   9.149 +  let
   9.150 +    val thy = ProofContext.theory_of ctxt;
   9.151 +    val target_name =
   9.152 +      [Pretty.command (if is_class then "class" else "locale"),
   9.153 +        Pretty.str (" " ^ Locale.extern thy target)];
   9.154 +    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
   9.155 +      (#1 (ProofContext.inferred_fixes ctxt));
   9.156 +    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
   9.157 +      (Assumption.all_assms_of ctxt);
   9.158 +    val elems =
   9.159 +      (if null fixes then [] else [Element.Fixes fixes]) @
   9.160 +      (if null assumes then [] else [Element.Assumes assumes]);
   9.161 +  in
   9.162 +    if target = "" then []
   9.163 +    else if null elems then [Pretty.block target_name]
   9.164 +    else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
   9.165 +      map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
   9.166 +  end;
   9.167 +
   9.168 +fun pretty (Target {target, is_class, ...}) ctxt =
   9.169 +  Pretty.block [Pretty.command "theory", Pretty.brk 1,
   9.170 +      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
   9.171 +    pretty_thy ctxt target is_class;
   9.172 +
   9.173 +
   9.174 +(* init various targets *)
   9.175 +
   9.176 +local
   9.177 +
   9.178 +fun init_data (Target {target, is_locale, is_class}) =
   9.179 +  if not is_locale then ProofContext.init_global
   9.180 +  else if not is_class then Locale.init target
   9.181 +  else Class_Target.init target;
   9.182 +
   9.183 +fun init_target (ta as Target {target, ...}) thy =
   9.184 +  thy
   9.185 +  |> init_data ta
   9.186 +  |> Data.put ta
   9.187 +  |> Local_Theory.init NONE (Long_Name.base_name target)
   9.188 +     {define = Generic_Target.define (target_foundation ta),
   9.189 +      notes = Generic_Target.notes (target_notes ta),
   9.190 +      abbrev = Generic_Target.abbrev (target_abbrev ta),
   9.191 +      declaration = fn pervasive => target_declaration ta
   9.192 +        { syntax = false, pervasive = pervasive },
   9.193 +      syntax_declaration = fn pervasive => target_declaration ta
   9.194 +        { syntax = true, pervasive = pervasive },
   9.195 +      pretty = pretty ta,
   9.196 +      reinit = init_target ta o ProofContext.theory_of,
   9.197 +      exit = Local_Theory.target_of};
   9.198 +
   9.199 +fun named_target _ NONE = global_target
   9.200 +  | named_target thy (SOME target) =
   9.201 +      if Locale.defined thy target
   9.202 +      then make_target target true (Class_Target.is_class thy target)
   9.203 +      else error ("No such locale: " ^ quote target);
   9.204 +
   9.205 +in
   9.206 +
   9.207 +fun init target thy = init_target (named_target thy target) thy;
   9.208 +
   9.209 +fun context_cmd "-" thy = init NONE thy
   9.210 +  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
   9.211 +
   9.212 +end;
   9.213 +
   9.214 +end;
    10.1 --- a/src/Pure/Isar/specification.ML	Wed Aug 11 14:41:16 2010 +0200
    10.2 +++ b/src/Pure/Isar/specification.ML	Wed Aug 11 14:45:38 2010 +0200
    10.3 @@ -185,7 +185,7 @@
    10.4  
    10.5      (*facts*)
    10.6      val (facts, facts_lthy) = axioms_thy
    10.7 -      |> Theory_Target.init NONE
    10.8 +      |> Named_Target.init NONE
    10.9        |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
   10.10        |> Local_Theory.notes axioms;
   10.11  
    11.1 --- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:41:16 2010 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,211 +0,0 @@
    11.4 -(*  Title:      Pure/Isar/theory_target.ML
    11.5 -    Author:     Makarius
    11.6 -    Author:     Florian Haftmann, TU Muenchen
    11.7 -
    11.8 -Common theory/locale/class/instantiation/overloading targets.
    11.9 -*)
   11.10 -
   11.11 -signature THEORY_TARGET =
   11.12 -sig
   11.13 -  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
   11.14 -  val init: string option -> theory -> local_theory
   11.15 -  val context_cmd: xstring -> theory -> local_theory
   11.16 -end;
   11.17 -
   11.18 -structure Theory_Target: THEORY_TARGET =
   11.19 -struct
   11.20 -
   11.21 -(* context data *)
   11.22 -
   11.23 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
   11.24 -
   11.25 -fun make_target target is_locale is_class =
   11.26 -  Target {target = target, is_locale = is_locale, is_class = is_class};
   11.27 -
   11.28 -val global_target = make_target "" false false;
   11.29 -
   11.30 -structure Data = Proof_Data
   11.31 -(
   11.32 -  type T = target;
   11.33 -  fun init _ = global_target;
   11.34 -);
   11.35 -
   11.36 -val peek = (fn Target args => args) o Data.get;
   11.37 -
   11.38 -
   11.39 -(* generic declarations *)
   11.40 -
   11.41 -fun locale_declaration locale { syntax, pervasive } decl lthy =
   11.42 -  let
   11.43 -    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
   11.44 -    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
   11.45 -  in
   11.46 -    lthy
   11.47 -    |> pervasive ? Generic_Target.theory_declaration decl
   11.48 -    |> Local_Theory.target (add locale locale_decl)
   11.49 -  end;
   11.50 -
   11.51 -fun target_declaration (Target {target, ...}) { syntax, pervasive } =
   11.52 -  if target = "" then Generic_Target.theory_declaration
   11.53 -  else locale_declaration target { syntax = syntax, pervasive = pervasive };
   11.54 -
   11.55 -
   11.56 -(* consts in locales *)
   11.57 -
   11.58 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
   11.59 -  let
   11.60 -    val b' = Morphism.binding phi b;
   11.61 -    val rhs' = Morphism.term phi rhs;
   11.62 -    val arg = (b', Term.close_schematic_term rhs');
   11.63 -    val same_shape = Term.aconv_untyped (rhs, rhs');
   11.64 -    (* FIXME workaround based on educated guess *)
   11.65 -    val prefix' = Binding.prefix_of b';
   11.66 -    val is_canonical_class = is_class andalso
   11.67 -      (Binding.eq_name (b, b')
   11.68 -        andalso not (null prefix')
   11.69 -        andalso List.last prefix' = (Class_Target.class_prefix target, false)
   11.70 -      orelse same_shape);
   11.71 -  in
   11.72 -    not is_canonical_class ?
   11.73 -      (Context.mapping_result
   11.74 -        (Sign.add_abbrev Print_Mode.internal arg)
   11.75 -        (ProofContext.add_abbrev Print_Mode.internal arg)
   11.76 -      #-> (fn (lhs' as Const (d, _), _) =>
   11.77 -          same_shape ?
   11.78 -            (Context.mapping
   11.79 -              (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
   11.80 -             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   11.81 -  end;
   11.82 -
   11.83 -fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
   11.84 -  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
   11.85 -
   11.86 -fun class_target (Target {target, ...}) f =
   11.87 -  Local_Theory.raw_theory f #>
   11.88 -  Local_Theory.target (Class_Target.refresh_syntax target);
   11.89 -
   11.90 -
   11.91 -(* define *)
   11.92 -
   11.93 -fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   11.94 -  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   11.95 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
   11.96 -    #> pair (lhs, def))
   11.97 -
   11.98 -fun class_foundation (ta as Target {target, ...})
   11.99 -    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
  11.100 -  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
  11.101 -  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
  11.102 -    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
  11.103 -    #> pair (lhs, def))
  11.104 -
  11.105 -fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
  11.106 -  if is_class then class_foundation ta
  11.107 -  else if is_locale then locale_foundation ta
  11.108 -  else Generic_Target.theory_foundation;
  11.109 -
  11.110 -
  11.111 -(* notes *)
  11.112 -
  11.113 -fun locale_notes locale kind global_facts local_facts lthy = 
  11.114 -  let
  11.115 -    val global_facts' = Attrib.map_facts (K I) global_facts;
  11.116 -    val local_facts' = Element.facts_map
  11.117 -      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
  11.118 -  in
  11.119 -    lthy
  11.120 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
  11.121 -    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
  11.122 -  end
  11.123 -
  11.124 -fun target_notes (ta as Target {target, is_locale, ...}) =
  11.125 -  if is_locale then locale_notes target
  11.126 -    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
  11.127 -
  11.128 -
  11.129 -(* abbrev *)
  11.130 -
  11.131 -fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
  11.132 -  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
  11.133 -    (fn (lhs, _) => locale_const_declaration ta prmode
  11.134 -      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
  11.135 -
  11.136 -fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
  11.137 -    prmode (b, mx) (global_rhs, t') xs lthy =
  11.138 -  if is_locale
  11.139 -    then lthy
  11.140 -      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
  11.141 -      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
  11.142 -    else lthy
  11.143 -      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
  11.144 -
  11.145 -
  11.146 -(* pretty *)
  11.147 -
  11.148 -fun pretty_thy ctxt target is_class =
  11.149 -  let
  11.150 -    val thy = ProofContext.theory_of ctxt;
  11.151 -    val target_name =
  11.152 -      [Pretty.command (if is_class then "class" else "locale"),
  11.153 -        Pretty.str (" " ^ Locale.extern thy target)];
  11.154 -    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
  11.155 -      (#1 (ProofContext.inferred_fixes ctxt));
  11.156 -    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
  11.157 -      (Assumption.all_assms_of ctxt);
  11.158 -    val elems =
  11.159 -      (if null fixes then [] else [Element.Fixes fixes]) @
  11.160 -      (if null assumes then [] else [Element.Assumes assumes]);
  11.161 -  in
  11.162 -    if target = "" then []
  11.163 -    else if null elems then [Pretty.block target_name]
  11.164 -    else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
  11.165 -      map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
  11.166 -  end;
  11.167 -
  11.168 -fun pretty (Target {target, is_class, ...}) ctxt =
  11.169 -  Pretty.block [Pretty.command "theory", Pretty.brk 1,
  11.170 -      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
  11.171 -    pretty_thy ctxt target is_class;
  11.172 -
  11.173 -
  11.174 -(* init various targets *)
  11.175 -
  11.176 -local
  11.177 -
  11.178 -fun init_data (Target {target, is_locale, is_class}) =
  11.179 -  if not is_locale then ProofContext.init_global
  11.180 -  else if not is_class then Locale.init target
  11.181 -  else Class_Target.init target;
  11.182 -
  11.183 -fun init_target (ta as Target {target, ...}) thy =
  11.184 -  thy
  11.185 -  |> init_data ta
  11.186 -  |> Data.put ta
  11.187 -  |> Local_Theory.init NONE (Long_Name.base_name target)
  11.188 -     {define = Generic_Target.define (target_foundation ta),
  11.189 -      notes = Generic_Target.notes (target_notes ta),
  11.190 -      abbrev = Generic_Target.abbrev (target_abbrev ta),
  11.191 -      declaration = fn pervasive => target_declaration ta
  11.192 -        { syntax = false, pervasive = pervasive },
  11.193 -      syntax_declaration = fn pervasive => target_declaration ta
  11.194 -        { syntax = true, pervasive = pervasive },
  11.195 -      pretty = pretty ta,
  11.196 -      reinit = init_target ta o ProofContext.theory_of,
  11.197 -      exit = Local_Theory.target_of};
  11.198 -
  11.199 -fun named_target _ NONE = global_target
  11.200 -  | named_target thy (SOME target) =
  11.201 -      if Locale.defined thy target
  11.202 -      then make_target target true (Class_Target.is_class thy target)
  11.203 -      else error ("No such locale: " ^ quote target);
  11.204 -
  11.205 -in
  11.206 -
  11.207 -fun init target thy = init_target (named_target thy target) thy;
  11.208 -
  11.209 -fun context_cmd "-" thy = init NONE thy
  11.210 -  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
  11.211 -
  11.212 -end;
  11.213 -
  11.214 -end;
    12.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:41:16 2010 +0200
    12.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:45:38 2010 +0200
    12.3 @@ -103,7 +103,7 @@
    12.4  
    12.5  (* local theory wrappers *)
    12.6  
    12.7 -val loc_init = Theory_Target.context_cmd;
    12.8 +val loc_init = Named_Target.context_cmd;
    12.9  val loc_exit = Local_Theory.exit_global;
   12.10  
   12.11  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   12.12 @@ -194,7 +194,7 @@
   12.13  
   12.14  (* print state *)
   12.15  
   12.16 -val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
   12.17 +val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
   12.18  
   12.19  fun print_state_context state =
   12.20    (case try node_of state of
    13.1 --- a/src/Pure/Isar/typedecl.ML	Wed Aug 11 14:41:16 2010 +0200
    13.2 +++ b/src/Pure/Isar/typedecl.ML	Wed Aug 11 14:45:38 2010 +0200
    13.3 @@ -75,7 +75,7 @@
    13.4    end;
    13.5  
    13.6  fun typedecl_global decl =
    13.7 -  Theory_Target.init NONE
    13.8 +  Named_Target.init NONE
    13.9    #> typedecl decl
   13.10    #> Local_Theory.exit_result_global Morphism.typ;
   13.11  
   13.12 @@ -115,7 +115,7 @@
   13.13  end;
   13.14  
   13.15  fun abbrev_global decl rhs =
   13.16 -  Theory_Target.init NONE
   13.17 +  Named_Target.init NONE
   13.18    #> abbrev decl rhs
   13.19    #> Local_Theory.exit_result_global (K I);
   13.20  
    14.1 --- a/src/Pure/ROOT.ML	Wed Aug 11 14:41:16 2010 +0200
    14.2 +++ b/src/Pure/ROOT.ML	Wed Aug 11 14:45:38 2010 +0200
    14.3 @@ -210,7 +210,7 @@
    14.4  use "Isar/overloading.ML";
    14.5  use "axclass.ML";
    14.6  use "Isar/class_target.ML";
    14.7 -use "Isar/theory_target.ML";
    14.8 +use "Isar/named_target.ML";
    14.9  use "Isar/expression.ML";
   14.10  use "Isar/class.ML";
   14.11  
    15.1 --- a/src/Tools/quickcheck.ML	Wed Aug 11 14:41:16 2010 +0200
    15.2 +++ b/src/Tools/quickcheck.ML	Wed Aug 11 14:45:38 2010 +0200
    15.3 @@ -219,7 +219,7 @@
    15.4        | strip t = t;
    15.5      val {goal = st, ...} = Proof.raw_goal state;
    15.6      val (gi, frees) = Logic.goal_params (prop_of st) i;
    15.7 -    val some_locale = case (#target o Theory_Target.peek) lthy
    15.8 +    val some_locale = case (#target o Named_Target.peek) lthy
    15.9       of "" => NONE
   15.10        | locale => SOME locale;
   15.11      val assms = if no_assms then [] else case some_locale