# 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)