src/Pure/Isar/expression.ML
changeset 51736 1f66d74b8ce3
parent 51734 d504e349e951
child 51737 718866dda2fa
     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 @@ -39,6 +39,8 @@
     1.4      (term list list * (string * morphism) list * morphism) * Proof.context
     1.5    val read_goal_expression: expression -> Proof.context ->
     1.6      (term list list * (string * morphism) list * morphism) * Proof.context
     1.7 +  val permanent_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
     1.8 +  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
     1.9    val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.10    val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.11      bool -> Proof.state -> Proof.state
    1.12 @@ -851,7 +853,8 @@
    1.13        note_eqns_register note add_registration reinit deps witss eqns attrss export export';
    1.14    in setup_proof after_qed propss eqns goal_ctxt end;
    1.15  
    1.16 -val activate_only = Context.proof_map ooo Locale.add_registration;
    1.17 +val activate_proof = Context.proof_map ooo Locale.add_registration;
    1.18 +val activate_local_theory = Local_Theory.target ooo activate_proof;
    1.19  val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.20  fun add_dependency locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
    1.21  
    1.22 @@ -864,7 +867,7 @@
    1.23        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.24    in
    1.25      generic_interpretation prep_expr parse_prop prep_attr setup_proof
    1.26 -      Attrib.local_notes activate_only I expression raw_eqns ctxt
    1.27 +      Attrib.local_notes activate_proof I expression raw_eqns ctxt
    1.28    end;
    1.29  
    1.30  fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns thy =
    1.31 @@ -885,6 +888,33 @@
    1.32  
    1.33  in
    1.34  
    1.35 +fun permanent_interpretation expression raw_eqns lthy =
    1.36 +  let
    1.37 +    val _ = Local_Theory.assert_bottom true lthy;
    1.38 +    val target = case Named_Target.peek lthy of
    1.39 +          SOME { target, ... } => target
    1.40 +        | NONE => error "Not in a named target";
    1.41 +    val is_theory = (target = "");
    1.42 +    val activate = if is_theory then add_registration else add_dependency target;
    1.43 +    val reinit = if is_theory then I else Named_Target.reinit lthy;
    1.44 +  in
    1.45 +    lthy
    1.46 +    |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.47 +        Local_Theory.notes_kind activate reinit expression raw_eqns
    1.48 +  end;
    1.49 +
    1.50 +fun ephemeral_interpretation expression raw_eqns lthy =
    1.51 +  let
    1.52 +    val _ = if Option.map #target (Named_Target.peek lthy) = SOME ""
    1.53 +      andalso Local_Theory.level lthy = 1
    1.54 +      then error "Not possible on level of global theory" else ();
    1.55 +  in
    1.56 +    lthy
    1.57 +    |> Local_Theory.mark_brittle
    1.58 +    |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
    1.59 +        Local_Theory.notes_kind activate_local_theory I expression raw_eqns
    1.60 +  end;
    1.61 +
    1.62  fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
    1.63  fun interpret_cmd x = gen_interpret read_goal_expression
    1.64    Syntax.parse_prop Attrib.intern_src x;