# HG changeset patch # User haftmann # Date 1194025980 -3600 # Node ID f9090ae5cec9f3183c2f6023f8d0301f575c6c2b # Parent 58146cb7bf44fb0f5961e0c3fd10eb8c75b33a94 clarified theory target interface diff -r 58146cb7bf44 -r f9090ae5cec9 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:52:59 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 02 18:53:00 2007 +0100 @@ -387,7 +387,7 @@ val _ = OuterSyntax.command "context" "enter local theory context" K.thy_decl (P.name --| P.begin >> (fn name => - Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd (SOME name)))); + Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd name))); (* locales *) diff -r 58146cb7bf44 -r f9090ae5cec9 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 02 18:52:59 2007 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 02 18:53:00 2007 +0100 @@ -8,9 +8,9 @@ signature THEORY_TARGET = sig val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} + val init: string option -> theory -> local_theory + val init_cmd: xstring -> theory -> local_theory val begin: string -> Proof.context -> local_theory - val init: string option -> theory -> local_theory - val init_cmd: xstring option -> theory -> local_theory end; structure TheoryTarget: THEORY_TARGET = @@ -20,13 +20,15 @@ datatype target = Target of {target: string, is_locale: bool, is_class: bool}; -fun make_target target is_locale is_class = - Target {target = target, is_locale = is_locale, is_class = is_class}; +fun make_target thy NONE = + Target {target = "", is_locale = false, is_class = false} + | make_target thy (SOME target) = + Target {target = target, is_locale = true, is_class = Class.is_class thy target}; structure Data = ProofDataFun ( type T = target; - fun init _ = make_target "" false false; + fun init thy = make_target thy NONE; ); val peek = (fn Target args => args) o Data.get; @@ -297,17 +299,21 @@ (* init and exit *) -fun begin target ctxt = +fun init_ctxt ta thy = let - val thy = ProofContext.theory_of ctxt; - val is_locale = target <> ""; - val is_class = Class.is_class thy target; - val ta = Target {target = target, is_locale = is_locale, is_class = is_class}; + val Target {target = target, is_locale = is_locale, is_class = is_class} = ta in - ctxt - |> Data.put ta + thy + |> (if is_locale then Locale.init target else ProofContext.init) |> is_class ? Class.init target - |> LocalTheory.init (NameSpace.base target) + end; + +fun init_ops ta init_ctxt = + let + val Target {target = target, ...} = ta; + in + Data.put ta + #> LocalTheory.init (NameSpace.base target) {pretty = pretty ta, axioms = axioms ta, abbrev = abbrev ta, @@ -317,15 +323,30 @@ term_syntax = term_syntax ta, declaration = declaration ta, target_naming = target_naming ta, - reinit = fn _ => - begin target o (if is_locale then Locale.init target else ProofContext.init), + reinit = fn _ => init_ops ta init_ctxt o init_ctxt, exit = LocalTheory.target_of} end; -fun init NONE thy = begin "" (ProofContext.init thy) - | init (SOME target) thy = begin target (Locale.init target thy); +fun init target thy = + let + val ta = make_target thy target; + val init_ctxt = init_ctxt ta; + in + thy + |> init_ctxt + |> init_ops ta init_ctxt + end; -fun init_cmd (SOME "-") thy = init NONE thy - | init_cmd target thy = init (Option.map (Locale.intern thy) target) thy; +fun begin target ctxt = + let + val thy = ProofContext.theory_of ctxt; + val ta = make_target thy (SOME target); + in + ctxt + |> init_ops ta (init_ctxt ta) + end; + +fun init_cmd "-" thy = init NONE thy + | init_cmd target thy = init (SOME (Locale.intern thy target)) thy; end; diff -r 58146cb7bf44 -r f9090ae5cec9 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Nov 02 18:52:59 2007 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Nov 02 18:53:00 2007 +0100 @@ -118,9 +118,10 @@ val loc_exit = ProofContext.theory_of o LocalTheory.exit; -fun loc_begin loc (Context.Theory thy) = loc_init loc thy +fun loc_begin NONE (Context.Theory thy) = loc_init "-" thy + | loc_begin (SOME loc) (Context.Theory thy) = loc_init loc thy | loc_begin NONE (Context.Proof lthy) = lthy - | loc_begin loc (Context.Proof lthy) = loc_init loc (loc_exit lthy); + | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore @@ -147,7 +148,7 @@ fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node | presentation_context (SOME node) (SOME loc) = - loc_init (SOME loc) (cases_node Context.theory_of Proof.theory_of node) + loc_init loc (cases_node Context.theory_of Proof.theory_of node) | presentation_context NONE _ = raise UNDEF; @@ -207,7 +208,7 @@ (* print state *) -val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I; +val pretty_context = LocalTheory.pretty o Context.cases (loc_init "-") I; fun print_state_context state = (case try node_of state of