# HG changeset patch
# User blanchet
# Date 1290533216 -3600
# Node ID 1a65f0c748275b194b4663634114f957a5686cf8
# Parent  e023788a91a1ae57beed53028e01481cfa4d75e2
added "verbose" option to Metis to shut up its warnings if necessary

diff -r e023788a91a1 -r 1a65f0c74827 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Nov 22 23:37:00 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Nov 23 18:26:56 2010 +0100
@@ -13,6 +13,8 @@
 
   val trace : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
+  val verbose : bool Config.T
+  val verbose_warning : Proof.context -> string -> unit
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term -> term -> bool
   val replay_one_inference :
@@ -30,8 +32,11 @@
 open Metis_Translate
 
 val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+fun verbose_warning ctxt msg =
+  if Config.get ctxt verbose then warning msg else ()
 
 datatype term_or_type = SomeTerm of term | SomeType of typ
 
@@ -821,6 +826,6 @@
                     \Error when discharging Skolem assumptions.")
     end
 
-val setup = trace_setup
+val setup = trace_setup #> verbose_setup
 
 end;
diff -r e023788a91a1 -r 1a65f0c74827 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Nov 22 23:37:00 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Nov 23 18:26:56 2010 +0100
@@ -10,6 +10,7 @@
 signature METIS_TACTICS =
 sig
   val trace : bool Config.T
+  val verbose : bool Config.T
   val type_lits : bool Config.T
   val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic
@@ -103,12 +104,12 @@
                   if have_common_thm used cls then NONE else SOME name)
             in
                 if not (null cls) andalso not (have_common_thm used cls) then
-                  warning "Metis: The assumptions are inconsistent."
+                  verbose_warning ctxt "Metis: The assumptions are inconsistent"
                 else
                   ();
                 if not (null unused) then
-                  warning ("Metis: Unused theorems: " ^ commas_quote unused
-                           ^ ".")
+                  verbose_warning ctxt ("Metis: Unused theorems: " ^
+                                        commas_quote unused)
                 else
                   ();
                 case result of
@@ -154,7 +155,8 @@
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   in
     if exists_type type_has_top_sort (prop_of st0) then
-      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
+      (verbose_warning ctxt "Metis: Proof state contains the universal sort {}";
+       Seq.empty)
     else
       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)