conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
authorwenzelm
Fri Apr 30 17:18:29 2010 +0200 (2010-04-30)
changeset 365455c5b5c7f1157
parent 36544 8da6846b87d9
child 36546 a9873318fe30
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 29 23:55:43 2010 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Apr 30 17:18:29 2010 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4    val the_context: simpset -> Proof.context
     1.5    val context: Proof.context -> simpset -> simpset
     1.6    val global_context: theory  -> simpset -> simpset
     1.7 +  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
     1.8    val debug_bounds: bool Unsynchronized.ref
     1.9    val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
    1.10    val set_solvers: solver list -> simpset -> simpset
    1.11 @@ -326,7 +327,8 @@
    1.12    print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
    1.13  
    1.14  fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
    1.15 -  if is_some context then () else warn_thm a ss th;
    1.16 +  if (case context of NONE => true | SOME ctxt => Context_Position.is_visible ctxt)
    1.17 +  then warn_thm a ss th else ();
    1.18  
    1.19  end;
    1.20  
    1.21 @@ -358,9 +360,13 @@
    1.22  fun activate_context thy ss =
    1.23    let
    1.24      val ctxt = the_context ss;
    1.25 -    val ctxt' = Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
    1.26 +    val ctxt' = ctxt
    1.27 +      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
    1.28 +      |> Context_Position.set_visible false;
    1.29    in context ctxt' ss end;
    1.30  
    1.31 +fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
    1.32 +
    1.33  
    1.34  (* maintain simp rules *)
    1.35  
     2.1 --- a/src/Pure/simplifier.ML	Thu Apr 29 23:55:43 2010 +0200
     2.2 +++ b/src/Pure/simplifier.ML	Fri Apr 30 17:18:29 2010 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4  );
     2.5  
     2.6  val get_ss = SimpsetData.get;
     2.7 -val map_ss = SimpsetData.map;
     2.8 +fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
     2.9  
    2.10  
    2.11  (* attributes *)