clarified theory target interface
authorhaftmann
Fri Nov 02 18:53:00 2007 +0100 (2007-11-02)
changeset 25269f9090ae5cec9
parent 25268 58146cb7bf44
child 25270 2ed7b34f58e6
clarified theory target interface
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	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