removed unused Theory_Target.begin;
authorwenzelm
Thu Feb 18 23:41:01 2010 +0100 (2010-02-18 ago)
changeset 35205611b90bb89bc
parent 35204 214ec053128e
child 35207 6f5b716b8500
removed unused Theory_Target.begin;
Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb;
renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern;
tuned;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 18 23:38:33 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 18 23:41:01 2010 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4  val _ =
     1.5    OuterSyntax.command "context" "enter local theory context" K.thy_decl
     1.6      (P.name --| P.begin >> (fn name =>
     1.7 -      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
     1.8 +      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
     1.9  
    1.10  
    1.11  (* locales *)
     2.1 --- a/src/Pure/Isar/theory_target.ML	Thu Feb 18 23:38:33 2010 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Feb 18 23:41:01 2010 +0100
     2.3 @@ -7,12 +7,14 @@
     2.4  
     2.5  signature THEORY_TARGET =
     2.6  sig
     2.7 -  val peek: local_theory -> {target: string, is_locale: bool,
     2.8 -    is_class: bool, instantiation: string list * (string * sort) list * sort,
     2.9 +  val peek: local_theory ->
    2.10 +   {target: string,
    2.11 +    is_locale: bool,
    2.12 +    is_class: bool,
    2.13 +    instantiation: string list * (string * sort) list * sort,
    2.14      overloading: (string * (string * typ) * bool) list}
    2.15    val init: string option -> theory -> local_theory
    2.16 -  val begin: string -> Proof.context -> local_theory
    2.17 -  val context: xstring -> theory -> local_theory
    2.18 +  val context_cmd: xstring -> theory -> local_theory
    2.19    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    2.20    val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    2.21    val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
    2.22 @@ -305,13 +307,13 @@
    2.23    in ((lhs, (res_name, res)), lthy4) end;
    2.24  
    2.25  
    2.26 -(* init *)
    2.27 +(* init various targets *)
    2.28  
    2.29  local
    2.30  
    2.31  fun init_target _ NONE = global_target
    2.32    | init_target thy (SOME target) =
    2.33 -      if Locale.defined thy (Locale.intern thy target)
    2.34 +      if Locale.defined thy target
    2.35        then make_target target true (Class_Target.is_class thy target) ([], [], []) []
    2.36        else error ("No such locale: " ^ quote target);
    2.37  
    2.38 @@ -349,17 +351,12 @@
    2.39  in
    2.40  
    2.41  fun init target thy = init_lthy_ctxt (init_target thy target) thy;
    2.42 -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
    2.43  
    2.44 -fun context "-" thy = init NONE thy
    2.45 -  | context target thy = init (SOME (Locale.intern thy target)) thy;
    2.46 -
    2.47 -
    2.48 -(* other targets *)
    2.49 +fun context_cmd "-" thy = init NONE thy
    2.50 +  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
    2.51  
    2.52  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    2.53 -fun instantiation_cmd raw_arities thy =
    2.54 -  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
    2.55 +fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy;
    2.56  
    2.57  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    2.58  val overloading_cmd = gen_overloading Syntax.read_term;
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Feb 18 23:38:33 2010 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Feb 18 23:41:01 2010 +0100
     3.3 @@ -104,7 +104,7 @@
     3.4  
     3.5  type generic_theory = Context.generic;    (*theory or local_theory*)
     3.6  
     3.7 -val loc_init = Theory_Target.context;
     3.8 +val loc_init = Theory_Target.context_cmd;
     3.9  val loc_exit = Local_Theory.exit_global;
    3.10  
    3.11  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy