tuned warnings: observe Context_Position.is_visible;
authorwenzelm
Sun Jan 11 21:06:47 2015 +0100 (2015-01-11)
changeset 5935263c02d051661
parent 59351 bb6eecfd7a55
child 59353 f0707dc3d9aa
child 59362 41f1645a4f63
tuned warnings: observe Context_Position.is_visible;
src/HOL/Library/refute.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/sat.ML
     1.1 --- a/src/HOL/Library/refute.ML	Sun Jan 11 20:45:03 2015 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sun Jan 11 21:06:47 2015 +0100
     1.3 @@ -1025,11 +1025,9 @@
     1.4                | NONE => false)
     1.5            | _ => false) types
     1.6          val _ =
     1.7 -          if maybe_spurious then
     1.8 -            warning ("Term contains a recursive datatype; "
     1.9 -              ^ "countermodel(s) may be spurious!")
    1.10 -          else
    1.11 -            ()
    1.12 +          if maybe_spurious andalso Context_Position.is_visible ctxt then
    1.13 +            warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
    1.14 +          else ()
    1.15          fun find_model_loop universe =
    1.16            let
    1.17              val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
    1.18 @@ -1056,7 +1054,7 @@
    1.19              val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
    1.20              val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
    1.21              val _ =
    1.22 -              (if member (op =) ["cdclite"] satsolver then
    1.23 +              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
    1.24                  warning ("Using SAT solver " ^ quote satsolver ^
    1.25                           "; for better performance, consider installing an \
    1.26                           \external solver.")
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 11 20:45:03 2015 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jan 11 21:06:47 2015 +0100
     2.3 @@ -434,7 +434,7 @@
     2.4  
     2.5      val (_ : unit list) = ctr_spec_eqn_data_list' |> map (fn (({ctr, ...}, nonexhaustive), x) =>
     2.6        if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
     2.7 -      else if length x = 1 orelse nonexhaustive then ()
     2.8 +      else if length x = 1 orelse nonexhaustive orelse not (Context_Position.is_visible ctxt) then ()
     2.9        else warning ("no equation for constructor " ^ Syntax.string_of_term ctxt ctr));
    2.10  
    2.11      val ctr_spec_eqn_data_list =
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Jan 11 20:45:03 2015 +0100
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Jan 11 21:06:47 2015 +0100
     3.3 @@ -301,11 +301,13 @@
     3.4            "Divides.div_class.mod" (*DYNAMIC BINDING!*),
     3.5            "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
     3.6      | _ =>
     3.7 -      (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
     3.8 -        false))
     3.9 +      (if Context_Position.is_visible ctxt then
    3.10 +        warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
    3.11 +       else (); false))
    3.12    | _ =>
    3.13 -    (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
    3.14 -      false));
    3.15 +    (if Context_Position.is_visible ctxt then
    3.16 +      warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
    3.17 +     else (); false));
    3.18  
    3.19  (* substitute new for occurrences of old in a term, incrementing bound       *)
    3.20  (* variables as needed when substituting inside an abstraction               *)
    3.21 @@ -637,12 +639,12 @@
    3.22      (* code exists above -- in which case either the split theorem should be *)
    3.23      (* implemented above, or 'is_split_thm' should be modified to filter it  *)
    3.24      (* out                                                                   *)
    3.25 -    | (t, ts) => (
    3.26 -      warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
    3.27 -        " (with " ^ string_of_int (length ts) ^
    3.28 -        " argument(s)) not implemented; proof reconstruction is likely to fail");
    3.29 -      NONE
    3.30 -    ))
    3.31 +    | (t, ts) =>
    3.32 +      (if Context_Position.is_visible ctxt then
    3.33 +        warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
    3.34 +          " (with " ^ string_of_int (length ts) ^
    3.35 +          " argument(s)) not implemented; proof reconstruction is likely to fail")
    3.36 +       else (); NONE))
    3.37  end;  (* split_once_items *)
    3.38  
    3.39  (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
     4.1 --- a/src/HOL/Tools/sat.ML	Sun Jan 11 20:45:03 2015 +0100
     4.2 +++ b/src/HOL/Tools/sat.ML	Sun Jan 11 21:06:47 2015 +0100
     4.3 @@ -291,9 +291,10 @@
     4.4      val clauses'' = filter (fn clause =>
     4.5        ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
     4.6          handle TERM ("dest_Trueprop", _) => false)
     4.7 -      orelse (
     4.8 -        warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
     4.9 -        false)) clauses'
    4.10 +      orelse
    4.11 +       (if Context_Position.is_visible ctxt then
    4.12 +          warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause))
    4.13 +        else (); false)) clauses'
    4.14      (* remove trivial clauses -- this is necessary because zChaff removes *)
    4.15      (* trivial clauses during preprocessing, and otherwise our clause     *)
    4.16      (* numbering would be off                                             *)
    4.17 @@ -372,7 +373,9 @@
    4.18            end)
    4.19      | SAT_Solver.UNSATISFIABLE NONE =>
    4.20          if Config.get ctxt quick_and_dirty then
    4.21 -         (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
    4.22 +         (if Context_Position.is_visible ctxt then
    4.23 +            warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"
    4.24 +          else ();
    4.25            make_quick_and_dirty_thm ())
    4.26          else
    4.27            raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])