Output.debug: non-strict;
renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
--- 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;
--- 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
--- 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
--- 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
);
--- 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)
--- 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);
--- 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)
--- 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) =
--- 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...*)
--- 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);
--- 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