# HG changeset patch
# User blanchet
# Date 1307436198 -7200
# Node ID 69f22ac07395cc5a038fe7bafd01112dafffe48f
# Parent  443708f05bb2b700ecebe8b0ab24c649ce8a285c
nicely thread monomorphism verbosity in Metis and Sledgehammer

diff -r 443708f05bb2 -r 69f22ac07395 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 07 08:58:23 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 07 10:43:18 2011 +0200
@@ -11,10 +11,6 @@
 sig
   exception METIS of string * string
 
-  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 hol_clause_from_metis :
     Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
     -> term
@@ -38,13 +34,6 @@
 
 exception METIS of string * string
 
-val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
-val verbose = Attrib.setup_config_bool @{binding metis_verbose} (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 ("Metis: " ^ msg) else ()
-
 datatype term_or_type = SomeTerm of term | SomeType of typ
 
 fun terms_of [] = []
diff -r 443708f05bb2 -r 69f22ac07395 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 08:58:23 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 10:43:18 2011 +0200
@@ -20,6 +20,10 @@
   val metis_app_op : string
   val metis_type_tag : string
   val metis_generated_var_prefix : string
+  val trace : bool Config.T
+  val verbose : bool Config.T
+  val trace_msg : Proof.context -> (unit -> string) -> unit
+  val verbose_warning : Proof.context -> string -> unit
   val metis_name_table : ((string * int) * (string * bool)) list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val prepare_metis_problem :
@@ -39,6 +43,13 @@
 val metis_type_tag = ":"
 val metis_generated_var_prefix = "_"
 
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (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 ("Metis: " ^ msg) else ()
+
 val metis_name_table =
   [((tptp_equal, 2), (metis_equal, false)),
    ((tptp_old_equal, 2), (metis_equal, false)),
@@ -163,7 +174,8 @@
             I
           else
             map (pair 0)
-            #> rpair ctxt
+            #> rpair (ctxt |> not (Config.get ctxt verbose)
+                              ? Config.put Monomorph.verbose false)
             #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
             #> fst #> maps (map (zero_var_indexes o snd)))
     val (old_skolems, props) =
diff -r 443708f05bb2 -r 69f22ac07395 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 08:58:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 10:43:18 2011 +0200
@@ -540,13 +540,13 @@
   |> minimize_command
 
 fun repair_monomorph_context debug max_iters max_new_instances =
-  Config.put Monomorph.verbose debug
+  (not debug ? Config.put Monomorph.verbose false)
   #> Config.put Monomorph.max_rounds max_iters
   #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.complete_instances false
 
 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
-  Config.put SMT_Config.verbose debug
+  (not debug ? Config.put SMT_Config.verbose false)
   #> Config.put SMT_Config.monomorph_limit max_mono_iters
   #> Config.put SMT_Config.monomorph_instances max_mono_instances
   #> Config.put SMT_Config.monomorph_full false