1.1 --- a/src/Pure/Isar/theory_target.ML Mon Nov 05 20:50:43 2007 +0100
1.2 +++ b/src/Pure/Isar/theory_target.ML Mon Nov 05 20:50:44 2007 +0100
1.3 @@ -9,8 +9,8 @@
1.4 sig
1.5 val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
1.6 val init: string option -> theory -> local_theory
1.7 - val init_cmd: xstring -> theory -> local_theory
1.8 val begin: string -> Proof.context -> local_theory
1.9 + val context: xstring -> theory -> local_theory
1.10 end;
1.11
1.12 structure TheoryTarget: THEORY_TARGET =
1.13 @@ -20,15 +20,15 @@
1.14
1.15 datatype target = Target of {target: string, is_locale: bool, is_class: bool};
1.16
1.17 -fun make_target thy NONE =
1.18 - Target {target = "", is_locale = false, is_class = false}
1.19 - | make_target thy (SOME target) =
1.20 - Target {target = target, is_locale = true, is_class = Class.is_class thy target};
1.21 +fun make_target target is_locale is_class =
1.22 + Target {target = target, is_locale = is_locale, is_class = is_class};
1.23 +
1.24 +val global_target = make_target "" false false;
1.25
1.26 structure Data = ProofDataFun
1.27 (
1.28 type T = target;
1.29 - fun init thy = make_target thy NONE;
1.30 + fun init _ = global_target;
1.31 );
1.32
1.33 val peek = (fn Target args => args) o Data.get;
1.34 @@ -297,56 +297,42 @@
1.35 end;
1.36
1.37
1.38 -(* init and exit *)
1.39 +(* init *)
1.40 +
1.41 +local
1.42
1.43 -fun init_ctxt ta thy =
1.44 - let
1.45 - val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
1.46 - in
1.47 - thy
1.48 - |> (if is_locale then Locale.init target else ProofContext.init)
1.49 - |> is_class ? Class.init target
1.50 - end;
1.51 +fun init_target _ NONE = global_target
1.52 + | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
1.53 +
1.54 +fun init_ctxt (Target {target, is_locale, is_class}) =
1.55 + (if is_locale then Locale.init target else ProofContext.init) #>
1.56 + is_class ? Class.init target;
1.57
1.58 -fun init_ops ta init_ctxt =
1.59 - let
1.60 - val Target {target = target, ...} = ta;
1.61 - in
1.62 - Data.put ta
1.63 - #> LocalTheory.init (NameSpace.base target)
1.64 - {pretty = pretty ta,
1.65 - axioms = axioms ta,
1.66 - abbrev = abbrev ta,
1.67 - define = define ta,
1.68 - notes = notes ta,
1.69 - type_syntax = type_syntax ta,
1.70 - term_syntax = term_syntax ta,
1.71 - declaration = declaration ta,
1.72 - target_naming = target_naming ta,
1.73 - reinit = fn _ => init_ops ta init_ctxt o init_ctxt,
1.74 - exit = LocalTheory.target_of}
1.75 - end;
1.76 +fun init_lthy (ta as Target {target, ...}) =
1.77 + Data.put ta #>
1.78 + LocalTheory.init (NameSpace.base target)
1.79 + {pretty = pretty ta,
1.80 + axioms = axioms ta,
1.81 + abbrev = abbrev ta,
1.82 + define = define ta,
1.83 + notes = notes ta,
1.84 + type_syntax = type_syntax ta,
1.85 + term_syntax = term_syntax ta,
1.86 + declaration = declaration ta,
1.87 + target_naming = target_naming ta,
1.88 + reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
1.89 + exit = LocalTheory.target_of}
1.90 +and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
1.91
1.92 -fun init target thy =
1.93 - let
1.94 - val ta = make_target thy target;
1.95 - val init_ctxt = init_ctxt ta;
1.96 - in
1.97 - thy
1.98 - |> init_ctxt
1.99 - |> init_ops ta init_ctxt
1.100 - end;
1.101 +in
1.102
1.103 -fun begin target ctxt =
1.104 - let
1.105 - val thy = ProofContext.theory_of ctxt;
1.106 - val ta = make_target thy (SOME target);
1.107 - in
1.108 - ctxt
1.109 - |> init_ops ta (init_ctxt ta)
1.110 - end;
1.111 +fun init target thy = init_lthy_ctxt (init_target thy target) thy;
1.112 +fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
1.113
1.114 -fun init_cmd "-" thy = init NONE thy
1.115 - | init_cmd target thy = init (SOME (Locale.intern thy target)) thy;
1.116 +fun context "-" thy = init NONE thy
1.117 + | context target thy = init (SOME (Locale.intern thy target)) thy;
1.118
1.119 end;
1.120 +
1.121 +end;
1.122 +