# HG changeset patch # User wenzelm # Date 1169298554 -3600 # Node ID 0906fd95e0b5fd54a855a1007fa11457b36a74b0 # Parent bb2203c93316af532dfeb2378c867e6158a75727 Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug); diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/ATP/reduce_axiomsN.ML --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Sat Jan 20 14:09:14 2007 +0100 @@ -184,7 +184,7 @@ in case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => defs lhs rhs andalso - (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true) + (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true) | _ => false end; @@ -201,15 +201,14 @@ else let val cls = sort compare_pairs newpairs val accepted = List.take (cls, !max_new) - in if !Output.show_debug_msgs then - (Output.debug ("Number of candidates, " ^ Int.toString nnew ^ - ", exceeds the limit of " ^ Int.toString (!max_new)); - Output.debug ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))); - Output.debug ("Actually passed: " ^ - space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted))) - else (); - (map #1 accepted, - map #1 (List.drop (cls, !max_new))) + in + Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ + ", exceeds the limit of " ^ Int.toString (!max_new))); + Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); + Output.debug (fn () => "Actually passed: " ^ + space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); + + (map #1 accepted, map #1 (List.drop (cls, !max_new))) end end; @@ -220,7 +219,8 @@ val new_consts = List.concat (map #2 newrels) val rel_consts' = foldl add_const_typ_table rel_consts new_consts val newp = p + (1.0-p) / !convergence - in Output.debug ("relevant this iteration: " ^ Int.toString (length newrels)); + in + Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); (map #1 newrels) @ (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects)) end @@ -228,28 +228,26 @@ let val weight = clause_weight ctab rel_consts consts_typs in if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts) - then (Output.debug (name ^ " passes: " ^ Real.toString weight); + then (Output.debug (fn () => (name ^ " passes: " ^ Real.toString weight)); relevant ((ax,weight)::newrels, rejects) axs) else relevant (newrels, ax::rejects) axs end - in Output.debug ("relevant_clauses, current pass mark = " ^ Real.toString p); + in Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); relevant ([],[]) end; fun relevance_filter thy axioms goals = if !run_relevance_filter andalso !pass_mark >= 0.1 then - let val _ = Output.debug "Start of relevance filtering"; + let val _ = Output.debug (fn () => "Start of relevance filtering"); val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals - val _ = if !Output.show_debug_msgs - then Output.debug ("Initial constants: " ^ - space_implode ", " (Symtab.keys goal_const_tab)) - else () + val _ = Output.debug (fn () => ("Initial constants: " ^ + space_implode ", " (Symtab.keys goal_const_tab))); val rels = relevant_clauses thy const_tab (!pass_mark) goal_const_tab (map (pair_consts_typs_axiom thy) axioms) in - Output.debug ("Total relevant: " ^ Int.toString (length rels)); + Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels))); rels end else axioms; diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Sat Jan 20 14:09:14 2007 +0100 @@ -45,7 +45,7 @@ val trace_path = Path.basic "watcher_trace"; -fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s else (); (*Representation of a watcher process*) @@ -236,7 +236,7 @@ in if childDone (*ATP has reported back (with success OR failure)*) then (Unix.reap proc_handle; - if !Output.show_debug_msgs then () else OS.FileSys.remove file; + if !Output.debugging then () else OS.FileSys.remove file; check children) else child :: check children end @@ -358,7 +358,7 @@ (goals_being_watched := !goals_being_watched - 1; if !goals_being_watched = 0 then - (Output.debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid); + (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid)); killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) else ()) fun proofHandler _ = @@ -369,9 +369,9 @@ val text = string_of_subgoal th sgno fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s); in - Output.debug ("In signal handler. outcome = \"" ^ outcome ^ + Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^ "\"\nprobfile = " ^ probfile ^ - "\nGoals being watched: "^ Int.toString (!goals_being_watched)); + "\nGoals being watched: "^ Int.toString (!goals_being_watched))); if String.isPrefix "Invalid" outcome then (report ("Subgoal is not provable:\n" ^ text); decr_watched()) @@ -389,7 +389,7 @@ else (report "System error in proof handler"; decr_watched()) end - in Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th); + in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th)); IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); (childin, childout, childpid) end diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Sat Jan 20 14:09:14 2007 +0100 @@ -349,14 +349,14 @@ val ih_intro = ihyp_thm RS inst_ex1_ex val ih_elim = ihyp_thm RS inst_ex1_un - val _ = Output.debug "Proving Replacement lemmas..." + val _ = Output.debug (fn () => "Proving Replacement lemmas...") val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses - val _ = Output.debug "Proving cases for unique existence..." + val _ = Output.debug (fn () => "Proving cases for unique existence...") val (ex1s, values) = split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) - val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *) + val _ = Output.debug (fn () => "Proving: Graph is a function") (* FIXME: Rewrite this proof. *) val graph_is_function = complete |> forall_elim_vars 0 |> fold (curry op COMP) ex1s diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/meson.ML Sat Jan 20 14:09:14 2007 +0100 @@ -271,7 +271,7 @@ and cnf_nil th = cnf_aux (th,[]) in if too_many_clauses (concl_of th) - then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths) + then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths) else cnf_aux (th,ths) end; @@ -574,12 +574,11 @@ [] => no_tac (*no goal clauses*) | goes => let val horns = make_horns (cls@ths) - val _ = if !Output.show_debug_msgs - then Output.debug ("meson method called:\n" ^ + val _ = + Output.debug (fn () => ("meson method called:\n" ^ space_implode "\n" (map string_of_thm (cls@ths)) ^ "\nclauses:\n" ^ - space_implode "\n" (map string_of_thm horns)) - else () + space_implode "\n" (map string_of_thm horns))) in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end ); diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/res_atp.ML Sat Jan 20 14:09:14 2007 +0100 @@ -56,7 +56,7 @@ structure ResAtp = struct -fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s); +fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s)); (********************************************************************) (* some settings for both background automatic ATP calling procedure*) @@ -237,7 +237,7 @@ else fn_lg f (FOL,seen) in if is_fol_logic lg' then () - else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f); + else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f)); term_lg (args@tms) (lg',seen') end | term_lg _ (lg,seen) = (lg,seen) @@ -261,7 +261,7 @@ else pred_lg pred (lg,seen) in if is_fol_logic lg' then () - else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred); + else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)); term_lg args (lg',seen') end; @@ -270,7 +270,7 @@ let val (lg,seen') = lit_lg lit (FOL,seen) in if is_fol_logic lg then () - else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit); + else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit)); lits_lg lits (lg,seen') end | lits_lg lits (lg,seen) = (lg,seen); @@ -288,7 +288,7 @@ let val (lg,seen') = logic_of_clause cls (FOL,seen) val _ = if is_fol_logic lg then () - else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls) + else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls)) in logic_of_clauses clss (lg,seen') end @@ -506,7 +506,7 @@ fun make_unique xs = let val ht = mk_clause_table 7000 in - Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses"); + Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht end; @@ -529,7 +529,7 @@ fun display_thms [] = () | display_thms ((name,thm)::nthms) = let val nthm = name ^ ": " ^ (string_of_thm thm) - in Output.debug nthm; display_thms nthms end; + in Output.debug (fn () => nthm); display_thms nthms end; fun all_valid_thms ctxt = PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @ @@ -571,7 +571,7 @@ let val included_thms = if !include_all then (tap (fn ths => Output.debug - ("Including all " ^ Int.toString (length ths) ^ " theorems")) + (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) (name_thm_pairs ctxt)) else let val claset_thms = @@ -583,8 +583,8 @@ val atpset_thms = if !include_atpset then ResAxioms.atpset_rules_of ctxt else [] - val _ = if !Output.show_debug_msgs - then (Output.debug "ATP theorems: "; display_thms atpset_thms) + val _ = if !Output.debugging + then (Output.debug (fn () => "ATP theorems: "); display_thms atpset_thms) else () in claset_thms @ simpset_thms @ atpset_thms end val user_rules = filter check_named @@ -600,12 +600,11 @@ let val banned = make_banned_test (map #1 ths) fun ok (a,_) = not (banned a) val (good,bad) = List.partition ok ths - in if !Output.show_debug_msgs then - (Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems"); - Output.debug("filtered: " ^ space_implode ", " (map #1 bad)); - Output.debug("...and returns " ^ Int.toString (length good))) - else (); - good + in + Output.debug (fn () => "blacklist filter gets " ^ Int.toString (length ths) ^ " theorems"); + Output.debug (fn () => "filtered: " ^ space_implode ", " (map #1 bad)); + Output.debug (fn () => "...and returns " ^ Int.toString (length good)); + good end else ths; @@ -751,14 +750,15 @@ and user_lemmas_names = map #1 user_rules in writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; - Output.debug ("Writing to " ^ file); + Output.debug (fn () => "Writing to " ^ file); file end; (**** remove tmp files ****) fun cond_rm_tmp file = - if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." + if !Output.debugging orelse !destdir <> "" + then Output.debug (fn () => "ATP input kept...") else OS.FileSys.remove file; @@ -785,7 +785,7 @@ val probfile = prob_pathname n val time = Int.toString (!time_limit) in - Output.debug ("problem file in watcher_call_provers is " ^ probfile); + Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile); (*options are separated by Watcher.setting_sep, currently #"%"*) if !prover = "spass" then @@ -816,7 +816,7 @@ val atp_list = make_atp_list sg_terms 1 in Watcher.callResProvers(childout,atp_list); - Output.debug "Sent commands to watcher!" + Output.debug (fn () => "Sent commands to watcher!") end fun trace_vector fname = @@ -829,7 +829,7 @@ subgoals, each involving &&.*) fun write_problem_files probfile (ctxt,th) = let val goals = Thm.prems_of th - val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) + val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals)) val thy = ProofContext.theory_of ctxt fun get_neg_subgoals [] _ = [] | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: @@ -844,11 +844,11 @@ |> ResAxioms.cnf_rules_pairs |> make_unique |> restrict_to_logic logic |> remove_unwanted_clauses - val _ = Output.debug ("included clauses = " ^ Int.toString(length included_cls)) + val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls)) val white_cls = ResAxioms.cnf_rules_pairs white_thms (*clauses relevant to goal gl*) val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls - val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls))) + val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) axcls_list val writer = if !prover = "spass" then dfg_writer else tptp_writer fun write_all [] [] _ = [] @@ -863,12 +863,12 @@ and tycons = type_consts_of_terms thy (ccltms@axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) val classrel_clauses = ResClause.make_classrel_clauses thy subs supers - val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) + val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses)) val arity_clauses = ResClause.arity_clause_thy thy tycons supers - val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) + val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses)) val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) [] val thm_names = Vector.fromList clnames - val _ = if !Output.show_debug_msgs + val _ = if !Output.debugging then trace_vector (fname ^ "_thm_names") thm_names else () in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) @@ -883,10 +883,10 @@ (case !last_watcher_pid of NONE => () | SOME (_, _, pid, files) => - (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); + (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid); Watcher.killWatcher pid; ignore (map (try cond_rm_tmp) files))) - handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; + handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed"); (*writes out the current problems and calls ATPs*) fun isar_atp (ctxt, th) = @@ -898,8 +898,8 @@ val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list) in last_watcher_pid := SOME (childin, childout, pid, files); - Output.debug ("problem files: " ^ space_implode ", " files); - Output.debug ("pid: " ^ string_of_pid pid); + Output.debug (fn () => "problem files: " ^ space_implode ", " files); + Output.debug (fn () => "pid: " ^ string_of_pid pid); watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) end; @@ -923,12 +923,12 @@ fun invoke_atp_ml (ctxt, goal) = let val thy = ProofContext.theory_of ctxt; in - Output.debug ("subgoals in isar_atp:\n" ^ + Output.debug (fn () => "subgoals in isar_atp:\n" ^ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); - Output.debug ("current theory: " ^ Context.theory_name thy); + Output.debug (fn () => "current theory: " ^ Context.theory_name thy); inc hook_count; - Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); + Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count)); ResClause.init thy; ResHolClause.init thy; if !time_limit > 0 then isar_atp (ctxt, goal) diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/res_axioms.ML Sat Jan 20 14:09:14 2007 +0100 @@ -467,7 +467,7 @@ It returns a modified theory, unless skolemization fails.*) fun skolem thy (name,th) = let val cname = (case name of "" => gensym "" | s => flatten_name s) - val _ = Output.debug ("skolemizing " ^ name ^ ": ") + val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ") in Option.map (fn nnfth => let val (thy',defs) = declare_skofuns cname nnfth thy @@ -495,28 +495,29 @@ end) | SOME (th',cls) => if eq_thm(th,th') then (cls,thy) - else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); - Output.debug (string_of_thm th); - Output.debug (string_of_thm th'); + else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name); + Output.debug (fn () => string_of_thm th); + Output.debug (fn () => string_of_thm th'); ([th],thy)); (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = - (Output.debug ("cnf_axiom called, theorem name = " ^ name); + (Output.debug (fn () => "cnf_axiom called, theorem name = " ^ name); case name of "" => skolem_thm th (*no name, so can't cache*) | s => case Symtab.lookup (!clause_cache) s of NONE => let val cls = map Goal.close_result (skolem_thm th) - in Output.debug "inserted into cache"; + in Output.debug (fn () => "inserted into cache"); change clause_cache (Symtab.update (s, (th, cls))); cls end | SOME(th',cls) => if eq_thm(th,th') then cls - else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); - Output.debug (string_of_thm th); - Output.debug (string_of_thm th'); - cls) + else + (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name); + Output.debug (fn () => string_of_thm th); + Output.debug (fn () => string_of_thm th'); + cls) ); fun pairname th = (PureThy.get_name_hint th, th); @@ -533,7 +534,7 @@ val intros = safeIs @ hazIs val elims = map Classical.classical_rule (safeEs @ hazEs) in - Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ + Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^ " elims: " ^ Int.toString(length elims)); map pairname (intros @ elims) end; @@ -542,8 +543,8 @@ let val ({rules,...}, _) = rep_ss ss val simps = Net.entries rules in - Output.debug ("rules_of_simpset: " ^ Int.toString(length simps)); - map (fn r => (#name r, #thm r)) simps + Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps)); + map (fn r => (#name r, #thm r)) simps end; fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/res_clause.ML Sat Jan 20 14:09:14 2007 +0100 @@ -425,7 +425,7 @@ fun make_axiom_clause thm (ax_name,cls_id) = if Meson.is_fol_term (prop_of thm) then (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE) - else (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); NONE) + else (Output.debug (fn () => ("Omitting " ^ ax_name ^ ": Axiom is not FOL")); NONE) fun make_axiom_clauses [] = [] | make_axiom_clauses ((thm,(name,id))::thms) = @@ -732,7 +732,7 @@ (* write out a subgoal in DFG format to the file "xxxx_N"*) fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = let - val _ = Output.debug ("Preparing to write the DFG file " ^ filename) + val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename)) val conjectures = make_conjecture_clauses thms val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures) @@ -818,7 +818,7 @@ (* write out a subgoal as tptp clauses to the file "xxxx_N"*) fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = let - val _ = Output.debug ("Preparing to write the TPTP file " ^ filename) + val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename)) val clss = make_conjecture_clauses thms val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples) val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss) diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Sat Jan 20 14:09:14 2007 +0100 @@ -536,19 +536,19 @@ val ct = foldl (count_user_clause user_lemmas) ct0 axclauses fun needed c = valOf (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" - then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) + then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) else [] val BC = if needed "c_COMBB" orelse needed "c_COMBC" - then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) + then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) else [] val S = if needed "c_COMBS" - then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) + then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) else [] val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" - then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) + then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C']) else [] val S' = if needed "c_COMBS_e" - then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) + then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S']) else [] val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] in @@ -579,7 +579,7 @@ fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals; fun display_arity (c,n) = - Output.debug ("Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ + Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ (if needs_hBOOL c then " needs hBOOL" else "")); fun count_constants (conjectures, axclauses, helper_clauses) = diff -r bb2203c93316 -r 0906fd95e0b5 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Sat Jan 20 14:09:14 2007 +0100 @@ -27,7 +27,7 @@ val trace_path = Path.basic "atp_trace"; -fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s else (); (*Full proof reconstruction wanted*) @@ -427,11 +427,9 @@ val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno val ccls = map forall_intr_vars ccls in - if !Output.show_debug_msgs - then app (Output.debug o string_of_thm) ccls - else (); - isar_header (map #1 fixes) ^ - String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)) + app (fn th => Output.debug (fn () => string_of_thm th)) ccls; + isar_header (map #1 fixes) ^ + String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)) end; (*Could use split_lines, but it can return blank lines...*) diff -r bb2203c93316 -r 0906fd95e0b5 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/Pure/General/output.ML Sat Jan 20 14:09:14 2007 +0100 @@ -27,7 +27,7 @@ val change_warn: ('b -> 'a -> bool) -> ('a -> 'b -> 'b) -> ('a -> string) -> 'a -> 'b -> 'b val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list - val show_debug_msgs: bool ref + val debugging: bool ref val no_warnings: ('a -> 'b) -> 'a -> 'b val timing: bool ref val cond_timeit: bool -> (unit -> 'a) -> 'a @@ -53,7 +53,7 @@ val ML_errors: ('a -> 'b) -> 'a -> 'b val panic: string -> unit val info: string -> unit - val debug: string -> unit + val debug: (unit -> string) -> unit val error_msg: string -> unit val ml_output: (string -> unit) * (string -> unit) val add_mode: string -> @@ -128,8 +128,8 @@ fun no_warnings f = setmp warning_fn (K ()) f; -val show_debug_msgs = ref false; -fun debug s = if ! show_debug_msgs then ! debug_fn (output s) else () +val debugging = ref false; +fun debug s = if ! debugging then ! debug_fn (output (s ())) else () fun error_msg s = ! error_fn (output s); diff -r bb2203c93316 -r 0906fd95e0b5 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sat Jan 20 14:09:12 2007 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Sat Jan 20 14:09:14 2007 +0100 @@ -133,9 +133,9 @@ bool_pref Output.timing "global-timing" "Whether to enable timing in Isabelle.", - bool_pref Output.show_debug_msgs - "debug-messages" - "Whether to show debugging messages."] + bool_pref Toplevel.debug + "debugging" + "Whether to enable debugging."] val proof_preferences = [bool_pref quick_and_dirty