# HG changeset patch
# User wenzelm
# Date 1421006807 -3600
# Node ID 63c02d05166146b48aa2aed682e86f4ab256f600
# Parent  bb6eecfd7a55af514ca584b354eb8d1ffff26256
tuned warnings: observe Context_Position.is_visible;

diff -r bb6eecfd7a55 -r 63c02d051661 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Library/refute.ML	Sun Jan 11 21:06:47 2015 +0100
@@ -1025,11 +1025,9 @@
               | NONE => false)
           | _ => false) types
         val _ =
-          if maybe_spurious then
-            warning ("Term contains a recursive datatype; "
-              ^ "countermodel(s) may be spurious!")
-          else
-            ()
+          if maybe_spurious andalso Context_Position.is_visible ctxt then
+            warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
+          else ()
         fun find_model_loop universe =
           let
             val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
@@ -1056,7 +1054,7 @@
             val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
             val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
             val _ =
-              (if member (op =) ["cdclite"] satsolver then
+              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
                 warning ("Using SAT solver " ^ quote satsolver ^
                          "; for better performance, consider installing an \
                          \external solver.")
diff -r bb6eecfd7a55 -r 63c02d051661 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 11 21:06:47 2015 +0100
@@ -434,7 +434,7 @@
 
     val (_ : unit list) = ctr_spec_eqn_data_list' |> map (fn (({ctr, ...}, nonexhaustive), x) =>
       if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
-      else if length x = 1 orelse nonexhaustive then ()
+      else if length x = 1 orelse nonexhaustive orelse not (Context_Position.is_visible ctxt) then ()
       else warning ("no equation for constructor " ^ Syntax.string_of_term ctxt ctr));
 
     val ctr_spec_eqn_data_list =
diff -r bb6eecfd7a55 -r 63c02d051661 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Jan 11 21:06:47 2015 +0100
@@ -301,11 +301,13 @@
           "Divides.div_class.mod" (*DYNAMIC BINDING!*),
           "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
     | _ =>
-      (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
-        false))
+      (if Context_Position.is_visible ctxt then
+        warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+       else (); false))
   | _ =>
-    (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
-      false));
+    (if Context_Position.is_visible ctxt then
+      warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+     else (); false));
 
 (* substitute new for occurrences of old in a term, incrementing bound       *)
 (* variables as needed when substituting inside an abstraction               *)
@@ -637,12 +639,12 @@
     (* code exists above -- in which case either the split theorem should be *)
     (* implemented above, or 'is_split_thm' should be modified to filter it  *)
     (* out                                                                   *)
-    | (t, ts) => (
-      warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
-        " (with " ^ string_of_int (length ts) ^
-        " argument(s)) not implemented; proof reconstruction is likely to fail");
-      NONE
-    ))
+    | (t, ts) =>
+      (if Context_Position.is_visible ctxt then
+        warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
+          " (with " ^ string_of_int (length ts) ^
+          " argument(s)) not implemented; proof reconstruction is likely to fail")
+       else (); NONE))
 end;  (* split_once_items *)
 
 (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
diff -r bb6eecfd7a55 -r 63c02d051661 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Sun Jan 11 20:45:03 2015 +0100
+++ b/src/HOL/Tools/sat.ML	Sun Jan 11 21:06:47 2015 +0100
@@ -291,9 +291,10 @@
     val clauses'' = filter (fn clause =>
       ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
         handle TERM ("dest_Trueprop", _) => false)
-      orelse (
-        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
-        false)) clauses'
+      orelse
+       (if Context_Position.is_visible ctxt then
+          warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause))
+        else (); false)) clauses'
     (* remove trivial clauses -- this is necessary because zChaff removes *)
     (* trivial clauses during preprocessing, and otherwise our clause     *)
     (* numbering would be off                                             *)
@@ -372,7 +373,9 @@
           end)
     | SAT_Solver.UNSATISFIABLE NONE =>
         if Config.get ctxt quick_and_dirty then
-         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
+         (if Context_Position.is_visible ctxt then
+            warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"
+          else ();
           make_quick_and_dirty_thm ())
         else
           raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])