1.1 --- a/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:52:59 2007 +0100
1.2 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:53:00 2007 +0100
1.3 @@ -387,7 +387,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 (TheoryTarget.init_cmd (SOME name))));
1.8 + Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd name)));
1.9
1.10
1.11 (* locales *)
2.1 --- a/src/Pure/Isar/theory_target.ML Fri Nov 02 18:52:59 2007 +0100
2.2 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 02 18:53:00 2007 +0100
2.3 @@ -8,9 +8,9 @@
2.4 signature THEORY_TARGET =
2.5 sig
2.6 val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
2.7 + val init: string option -> theory -> local_theory
2.8 + val init_cmd: xstring -> theory -> local_theory
2.9 val begin: string -> Proof.context -> local_theory
2.10 - val init: string option -> theory -> local_theory
2.11 - val init_cmd: xstring option -> theory -> local_theory
2.12 end;
2.13
2.14 structure TheoryTarget: THEORY_TARGET =
2.15 @@ -20,13 +20,15 @@
2.16
2.17 datatype target = Target of {target: string, is_locale: bool, is_class: bool};
2.18
2.19 -fun make_target target is_locale is_class =
2.20 - Target {target = target, is_locale = is_locale, is_class = is_class};
2.21 +fun make_target thy NONE =
2.22 + Target {target = "", is_locale = false, is_class = false}
2.23 + | make_target thy (SOME target) =
2.24 + Target {target = target, is_locale = true, is_class = Class.is_class thy target};
2.25
2.26 structure Data = ProofDataFun
2.27 (
2.28 type T = target;
2.29 - fun init _ = make_target "" false false;
2.30 + fun init thy = make_target thy NONE;
2.31 );
2.32
2.33 val peek = (fn Target args => args) o Data.get;
2.34 @@ -297,17 +299,21 @@
2.35
2.36 (* init and exit *)
2.37
2.38 -fun begin target ctxt =
2.39 +fun init_ctxt ta thy =
2.40 let
2.41 - val thy = ProofContext.theory_of ctxt;
2.42 - val is_locale = target <> "";
2.43 - val is_class = Class.is_class thy target;
2.44 - val ta = Target {target = target, is_locale = is_locale, is_class = is_class};
2.45 + val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
2.46 in
2.47 - ctxt
2.48 - |> Data.put ta
2.49 + thy
2.50 + |> (if is_locale then Locale.init target else ProofContext.init)
2.51 |> is_class ? Class.init target
2.52 - |> LocalTheory.init (NameSpace.base target)
2.53 + end;
2.54 +
2.55 +fun init_ops ta init_ctxt =
2.56 + let
2.57 + val Target {target = target, ...} = ta;
2.58 + in
2.59 + Data.put ta
2.60 + #> LocalTheory.init (NameSpace.base target)
2.61 {pretty = pretty ta,
2.62 axioms = axioms ta,
2.63 abbrev = abbrev ta,
2.64 @@ -317,15 +323,30 @@
2.65 term_syntax = term_syntax ta,
2.66 declaration = declaration ta,
2.67 target_naming = target_naming ta,
2.68 - reinit = fn _ =>
2.69 - begin target o (if is_locale then Locale.init target else ProofContext.init),
2.70 + reinit = fn _ => init_ops ta init_ctxt o init_ctxt,
2.71 exit = LocalTheory.target_of}
2.72 end;
2.73
2.74 -fun init NONE thy = begin "" (ProofContext.init thy)
2.75 - | init (SOME target) thy = begin target (Locale.init target thy);
2.76 +fun init target thy =
2.77 + let
2.78 + val ta = make_target thy target;
2.79 + val init_ctxt = init_ctxt ta;
2.80 + in
2.81 + thy
2.82 + |> init_ctxt
2.83 + |> init_ops ta init_ctxt
2.84 + end;
2.85
2.86 -fun init_cmd (SOME "-") thy = init NONE thy
2.87 - | init_cmd target thy = init (Option.map (Locale.intern thy) target) thy;
2.88 +fun begin target ctxt =
2.89 + let
2.90 + val thy = ProofContext.theory_of ctxt;
2.91 + val ta = make_target thy (SOME target);
2.92 + in
2.93 + ctxt
2.94 + |> init_ops ta (init_ctxt ta)
2.95 + end;
2.96 +
2.97 +fun init_cmd "-" thy = init NONE thy
2.98 + | init_cmd target thy = init (SOME (Locale.intern thy target)) thy;
2.99
2.100 end;
3.1 --- a/src/Pure/Isar/toplevel.ML Fri Nov 02 18:52:59 2007 +0100
3.2 +++ b/src/Pure/Isar/toplevel.ML Fri Nov 02 18:53:00 2007 +0100
3.3 @@ -118,9 +118,10 @@
3.4
3.5 val loc_exit = ProofContext.theory_of o LocalTheory.exit;
3.6
3.7 -fun loc_begin loc (Context.Theory thy) = loc_init loc thy
3.8 +fun loc_begin NONE (Context.Theory thy) = loc_init "-" thy
3.9 + | loc_begin (SOME loc) (Context.Theory thy) = loc_init loc thy
3.10 | loc_begin NONE (Context.Proof lthy) = lthy
3.11 - | loc_begin loc (Context.Proof lthy) = loc_init loc (loc_exit lthy);
3.12 + | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
3.13
3.14 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
3.15 | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
3.16 @@ -147,7 +148,7 @@
3.17 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
3.18 | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
3.19 | presentation_context (SOME node) (SOME loc) =
3.20 - loc_init (SOME loc) (cases_node Context.theory_of Proof.theory_of node)
3.21 + loc_init loc (cases_node Context.theory_of Proof.theory_of node)
3.22 | presentation_context NONE _ = raise UNDEF;
3.23
3.24
3.25 @@ -207,7 +208,7 @@
3.26
3.27 (* print state *)
3.28
3.29 -val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I;
3.30 +val pretty_context = LocalTheory.pretty o Context.cases (loc_init "-") I;
3.31
3.32 fun print_state_context state =
3.33 (case try node_of state of