src/Pure/Isar/theory_target.ML
changeset 25269 f9090ae5cec9
parent 25240 ff5815d04c23
child 25291 870455627720
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 02 18:52:59 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 02 18:53:00 2007 +0100
     1.3 @@ -8,9 +8,9 @@
     1.4  signature THEORY_TARGET =
     1.5  sig
     1.6    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
     1.7 +  val init: string option -> theory -> local_theory
     1.8 +  val init_cmd: xstring -> theory -> local_theory
     1.9    val begin: string -> Proof.context -> local_theory
    1.10 -  val init: string option -> theory -> local_theory
    1.11 -  val init_cmd: xstring option -> theory -> local_theory
    1.12  end;
    1.13  
    1.14  structure TheoryTarget: THEORY_TARGET =
    1.15 @@ -20,13 +20,15 @@
    1.16  
    1.17  datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    1.18  
    1.19 -fun make_target target is_locale is_class =
    1.20 -  Target {target = target, is_locale = is_locale, is_class = is_class};
    1.21 +fun make_target thy NONE =
    1.22 +      Target {target = "", is_locale = false, is_class = false}
    1.23 +  | make_target thy (SOME target) =
    1.24 +      Target {target = target, is_locale = true, is_class = Class.is_class thy target};
    1.25  
    1.26  structure Data = ProofDataFun
    1.27  (
    1.28    type T = target;
    1.29 -  fun init _ = make_target "" false false;
    1.30 +  fun init thy = make_target thy NONE;
    1.31  );
    1.32  
    1.33  val peek = (fn Target args => args) o Data.get;
    1.34 @@ -297,17 +299,21 @@
    1.35  
    1.36  (* init and exit *)
    1.37  
    1.38 -fun begin target ctxt =
    1.39 +fun init_ctxt ta thy =
    1.40    let
    1.41 -    val thy = ProofContext.theory_of ctxt;
    1.42 -    val is_locale = target <> "";
    1.43 -    val is_class = Class.is_class thy target;
    1.44 -    val ta = Target {target = target, is_locale = is_locale, is_class = is_class};
    1.45 +    val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
    1.46    in
    1.47 -    ctxt
    1.48 -    |> Data.put ta
    1.49 +    thy
    1.50 +    |> (if is_locale then Locale.init target else ProofContext.init)
    1.51      |> is_class ? Class.init target
    1.52 -    |> LocalTheory.init (NameSpace.base target)
    1.53 +  end;
    1.54 +
    1.55 +fun init_ops ta init_ctxt =
    1.56 +  let
    1.57 +    val Target {target = target, ...} = ta;
    1.58 +  in
    1.59 +    Data.put ta
    1.60 +    #> LocalTheory.init (NameSpace.base target)
    1.61       {pretty = pretty ta,
    1.62        axioms = axioms ta,
    1.63        abbrev = abbrev ta,
    1.64 @@ -317,15 +323,30 @@
    1.65        term_syntax = term_syntax ta,
    1.66        declaration = declaration ta,
    1.67        target_naming = target_naming ta,
    1.68 -      reinit = fn _ =>
    1.69 -        begin target o (if is_locale then Locale.init target else ProofContext.init),
    1.70 +      reinit = fn _ => init_ops ta init_ctxt o init_ctxt,
    1.71        exit = LocalTheory.target_of}
    1.72    end;
    1.73  
    1.74 -fun init NONE thy = begin "" (ProofContext.init thy)
    1.75 -  | init (SOME target) thy = begin target (Locale.init target thy);
    1.76 +fun init target thy =
    1.77 +  let
    1.78 +    val ta = make_target thy target;
    1.79 +    val init_ctxt = init_ctxt ta;
    1.80 +  in
    1.81 +    thy
    1.82 +    |> init_ctxt
    1.83 +    |> init_ops ta init_ctxt
    1.84 +  end;
    1.85  
    1.86 -fun init_cmd (SOME "-") thy = init NONE thy
    1.87 -  | init_cmd target thy = init (Option.map (Locale.intern thy) target) thy;
    1.88 +fun begin target ctxt =
    1.89 +  let
    1.90 +    val thy = ProofContext.theory_of ctxt;
    1.91 +    val ta = make_target thy (SOME target);
    1.92 +  in
    1.93 +    ctxt
    1.94 +    |> init_ops ta (init_ctxt ta)
    1.95 +  end;
    1.96 +
    1.97 +fun init_cmd "-" thy = init NONE thy
    1.98 +  | init_cmd target thy = init (SOME (Locale.intern thy target)) thy;
    1.99  
   1.100  end;