src/HOL/Tools/meson.ML
changeset 32955 4a78daeb012b
parent 32740 9dd0a2f83429
child 32960 69916a850301
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Oct 16 00:26:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Oct 16 10:45:10 2009 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature MESON =
     1.6  sig
     1.7 +  val trace: bool Unsynchronized.ref
     1.8    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     1.9    val first_order_resolve: thm -> thm -> thm
    1.10    val flexflex_first_order: thm -> thm
    1.11 @@ -42,6 +43,9 @@
    1.12  structure Meson: MESON =
    1.13  struct
    1.14  
    1.15 +val trace = Unsynchronized.ref false;
    1.16 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.17 +
    1.18  val max_clauses_default = 60;
    1.19  val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
    1.20  
    1.21 @@ -344,7 +348,7 @@
    1.22        and cnf_nil th = cnf_aux (th,[])
    1.23        val cls = 
    1.24  	    if too_many_clauses (SOME ctxt) (concl_of th)
    1.25 -	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.26 +	    then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.27  	    else cnf_aux (th,ths)
    1.28    in  (cls, !ctxtr)  end;
    1.29  
    1.30 @@ -547,7 +551,7 @@
    1.31    | skolemize_nnf_list ctxt (th::ths) =
    1.32        skolemize ctxt th :: skolemize_nnf_list ctxt ths
    1.33        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
    1.34 -       (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    1.35 +       (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    1.36          skolemize_nnf_list ctxt ths);
    1.37  
    1.38  fun add_clauses (th,cls) =
    1.39 @@ -636,7 +640,7 @@
    1.40      | goes =>
    1.41          let
    1.42            val horns = make_horns (cls @ ths)
    1.43 -          val _ = Output.debug (fn () =>
    1.44 +          val _ = trace_msg (fn () =>
    1.45              cat_lines ("meson method called:" ::
    1.46                map (Display.string_of_thm ctxt) (cls @ ths) @
    1.47                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))