src/Pure/Isar/expression.ML
changeset 51737 718866dda2fa
parent 51736 1f66d74b8ce3
child 51748 789507cd689d
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 23 11:14:50 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 23 11:14:50 2013 +0200
     1.3 @@ -44,11 +44,13 @@
     1.4    val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
     1.5    val interpret_cmd: expression -> (Attrib.binding * string) list ->
     1.6      bool -> Proof.state -> Proof.state
     1.7 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
     1.8 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
     1.9 -  val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    1.10 +  val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.11 +  val interpretation_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.12 +  val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.13 +  val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.14 +  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
    1.15      (Attrib.binding * term) list -> theory -> Proof.state
    1.16 -  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    1.17 +  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    1.18      (Attrib.binding * string) list -> theory -> Proof.state
    1.19  
    1.20    (* Diagnostic *)
    1.21 @@ -855,8 +857,10 @@
    1.22  
    1.23  val activate_proof = Context.proof_map ooo Locale.add_registration;
    1.24  val activate_local_theory = Local_Theory.target ooo activate_proof;
    1.25 -val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.26 -fun add_dependency locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.27 +val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    1.28 +val add_registration_global = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.29 +fun add_dependency locale = Local_Theory.raw_theory ooo Locale.add_dependency locale;
    1.30 +fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.31  
    1.32  fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
    1.33    let
    1.34 @@ -870,20 +874,37 @@
    1.35        Attrib.local_notes activate_proof I expression raw_eqns ctxt
    1.36    end;
    1.37  
    1.38 -fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns thy =
    1.39 -  thy
    1.40 -  |> Named_Target.theory_init
    1.41 -  |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.42 -      Local_Theory.notes_kind add_registration I expression raw_eqns;
    1.43 +fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
    1.44 +  let
    1.45 +    val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
    1.46 +      andalso Local_Theory.level lthy = 1;
    1.47 +    val activate = if is_theory then add_registration else activate_local_theory;
    1.48 +  in
    1.49 +    lthy
    1.50 +    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.51 +        Local_Theory.notes_kind activate I expression raw_eqns
    1.52 +  end;
    1.53  
    1.54 -fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    1.55 +fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
    1.56 +  let
    1.57 +    val locale =
    1.58 +      case Option.map #target (Named_Target.peek lthy) of
    1.59 +          SOME locale => locale
    1.60 +        | _ => error "Not in a locale target";
    1.61 +  in
    1.62 +    lthy
    1.63 +    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.64 +        Local_Theory.notes_kind (add_dependency locale) (Named_Target.reinit lthy) expression raw_eqns
    1.65 +  end;
    1.66 +  
    1.67 +fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
    1.68    let
    1.69      val locale = prep_loc thy raw_locale;
    1.70    in
    1.71      thy
    1.72      |> Named_Target.init before_exit locale
    1.73      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.74 -        Local_Theory.notes_kind (add_dependency locale) I expression raw_eqns
    1.75 +        Local_Theory.notes_kind (add_dependency_global locale) I expression raw_eqns
    1.76    end;
    1.77  
    1.78  in
    1.79 @@ -916,16 +937,20 @@
    1.80    end;
    1.81  
    1.82  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
    1.83 -fun interpret_cmd x = gen_interpret read_goal_expression
    1.84 -  Syntax.parse_prop Attrib.intern_src x;
    1.85 +fun interpret_cmd x =
    1.86 +  gen_interpret read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    1.87  
    1.88  fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
    1.89 -fun interpretation_cmd x = gen_interpretation read_goal_expression
    1.90 -  Syntax.parse_prop Attrib.intern_src x;
    1.91 +fun interpretation_cmd x =
    1.92 +  gen_interpretation read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    1.93  
    1.94 -fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    1.95 +fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) x;
    1.96  fun sublocale_cmd x =
    1.97 -  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
    1.98 +  gen_sublocale read_goal_expression Syntax.parse_prop Attrib.intern_src x;
    1.99 +
   1.100 +fun sublocale_global x = gen_sublocale_global cert_goal_expression (K I) (K I) (K I) x;
   1.101 +fun sublocale_global_cmd x =
   1.102 +  gen_sublocale_global read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
   1.103  
   1.104  end;
   1.105