1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Sat Jan 20 14:09:12 2007 +0100
1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Sat Jan 20 14:09:14 2007 +0100
1.3 @@ -184,7 +184,7 @@
1.4 in
1.5 case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
1.6 defs lhs rhs andalso
1.7 - (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
1.8 + (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
1.9 | _ => false
1.10 end;
1.11
1.12 @@ -201,15 +201,14 @@
1.13 else
1.14 let val cls = sort compare_pairs newpairs
1.15 val accepted = List.take (cls, !max_new)
1.16 - in if !Output.show_debug_msgs then
1.17 - (Output.debug ("Number of candidates, " ^ Int.toString nnew ^
1.18 - ", exceeds the limit of " ^ Int.toString (!max_new));
1.19 - Output.debug ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)));
1.20 - Output.debug ("Actually passed: " ^
1.21 - space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)))
1.22 - else ();
1.23 - (map #1 accepted,
1.24 - map #1 (List.drop (cls, !max_new)))
1.25 + in
1.26 + Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^
1.27 + ", exceeds the limit of " ^ Int.toString (!max_new)));
1.28 + Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
1.29 + Output.debug (fn () => "Actually passed: " ^
1.30 + space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
1.31 +
1.32 + (map #1 accepted, map #1 (List.drop (cls, !max_new)))
1.33 end
1.34 end;
1.35
1.36 @@ -220,7 +219,8 @@
1.37 val new_consts = List.concat (map #2 newrels)
1.38 val rel_consts' = foldl add_const_typ_table rel_consts new_consts
1.39 val newp = p + (1.0-p) / !convergence
1.40 - in Output.debug ("relevant this iteration: " ^ Int.toString (length newrels));
1.41 + in
1.42 + Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
1.43 (map #1 newrels) @
1.44 (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
1.45 end
1.46 @@ -228,28 +228,26 @@
1.47 let val weight = clause_weight ctab rel_consts consts_typs
1.48 in
1.49 if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
1.50 - then (Output.debug (name ^ " passes: " ^ Real.toString weight);
1.51 + then (Output.debug (fn () => (name ^ " passes: " ^ Real.toString weight));
1.52 relevant ((ax,weight)::newrels, rejects) axs)
1.53 else relevant (newrels, ax::rejects) axs
1.54 end
1.55 - in Output.debug ("relevant_clauses, current pass mark = " ^ Real.toString p);
1.56 + in Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
1.57 relevant ([],[])
1.58 end;
1.59
1.60 fun relevance_filter thy axioms goals =
1.61 if !run_relevance_filter andalso !pass_mark >= 0.1
1.62 then
1.63 - let val _ = Output.debug "Start of relevance filtering";
1.64 + let val _ = Output.debug (fn () => "Start of relevance filtering");
1.65 val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
1.66 val goal_const_tab = get_goal_consts_typs thy goals
1.67 - val _ = if !Output.show_debug_msgs
1.68 - then Output.debug ("Initial constants: " ^
1.69 - space_implode ", " (Symtab.keys goal_const_tab))
1.70 - else ()
1.71 + val _ = Output.debug (fn () => ("Initial constants: " ^
1.72 + space_implode ", " (Symtab.keys goal_const_tab)));
1.73 val rels = relevant_clauses thy const_tab (!pass_mark)
1.74 goal_const_tab (map (pair_consts_typs_axiom thy) axioms)
1.75 in
1.76 - Output.debug ("Total relevant: " ^ Int.toString (length rels));
1.77 + Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
1.78 rels
1.79 end
1.80 else axioms;
2.1 --- a/src/HOL/Tools/ATP/watcher.ML Sat Jan 20 14:09:12 2007 +0100
2.2 +++ b/src/HOL/Tools/ATP/watcher.ML Sat Jan 20 14:09:14 2007 +0100
2.3 @@ -45,7 +45,7 @@
2.4
2.5 val trace_path = Path.basic "watcher_trace";
2.6
2.7 -fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
2.8 +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
2.9 else ();
2.10
2.11 (*Representation of a watcher process*)
2.12 @@ -236,7 +236,7 @@
2.13 in
2.14 if childDone (*ATP has reported back (with success OR failure)*)
2.15 then (Unix.reap proc_handle;
2.16 - if !Output.show_debug_msgs then () else OS.FileSys.remove file;
2.17 + if !Output.debugging then () else OS.FileSys.remove file;
2.18 check children)
2.19 else child :: check children
2.20 end
2.21 @@ -358,7 +358,7 @@
2.22 (goals_being_watched := !goals_being_watched - 1;
2.23 if !goals_being_watched = 0
2.24 then
2.25 - (Output.debug ("\nReaping a watcher, childpid = " ^ string_of_pid childpid);
2.26 + (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
2.27 killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
2.28 else ())
2.29 fun proofHandler _ =
2.30 @@ -369,9 +369,9 @@
2.31 val text = string_of_subgoal th sgno
2.32 fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
2.33 in
2.34 - Output.debug ("In signal handler. outcome = \"" ^ outcome ^
2.35 + Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
2.36 "\"\nprobfile = " ^ probfile ^
2.37 - "\nGoals being watched: "^ Int.toString (!goals_being_watched));
2.38 + "\nGoals being watched: "^ Int.toString (!goals_being_watched)));
2.39 if String.isPrefix "Invalid" outcome
2.40 then (report ("Subgoal is not provable:\n" ^ text);
2.41 decr_watched())
2.42 @@ -389,7 +389,7 @@
2.43 else (report "System error in proof handler";
2.44 decr_watched())
2.45 end
2.46 - in Output.debug ("subgoals forked to createWatcher: "^ prems_string_of th);
2.47 + in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
2.48 IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
2.49 (childin, childout, childpid)
2.50 end
3.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML Sat Jan 20 14:09:12 2007 +0100
3.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Sat Jan 20 14:09:14 2007 +0100
3.3 @@ -349,14 +349,14 @@
3.4 val ih_intro = ihyp_thm RS inst_ex1_ex
3.5 val ih_elim = ihyp_thm RS inst_ex1_un
3.6
3.7 - val _ = Output.debug "Proving Replacement lemmas..."
3.8 + val _ = Output.debug (fn () => "Proving Replacement lemmas...")
3.9 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
3.10
3.11 - val _ = Output.debug "Proving cases for unique existence..."
3.12 + val _ = Output.debug (fn () => "Proving cases for unique existence...")
3.13 val (ex1s, values) =
3.14 split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
3.15
3.16 - val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
3.17 + val _ = Output.debug (fn () => "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
3.18 val graph_is_function = complete
3.19 |> forall_elim_vars 0
3.20 |> fold (curry op COMP) ex1s
4.1 --- a/src/HOL/Tools/meson.ML Sat Jan 20 14:09:12 2007 +0100
4.2 +++ b/src/HOL/Tools/meson.ML Sat Jan 20 14:09:14 2007 +0100
4.3 @@ -271,7 +271,7 @@
4.4 and cnf_nil th = cnf_aux (th,[])
4.5 in
4.6 if too_many_clauses (concl_of th)
4.7 - then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
4.8 + then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
4.9 else cnf_aux (th,ths)
4.10 end;
4.11
4.12 @@ -574,12 +574,11 @@
4.13 [] => no_tac (*no goal clauses*)
4.14 | goes =>
4.15 let val horns = make_horns (cls@ths)
4.16 - val _ = if !Output.show_debug_msgs
4.17 - then Output.debug ("meson method called:\n" ^
4.18 + val _ =
4.19 + Output.debug (fn () => ("meson method called:\n" ^
4.20 space_implode "\n" (map string_of_thm (cls@ths)) ^
4.21 "\nclauses:\n" ^
4.22 - space_implode "\n" (map string_of_thm horns))
4.23 - else ()
4.24 + space_implode "\n" (map string_of_thm horns)))
4.25 in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
4.26 end
4.27 );
5.1 --- a/src/HOL/Tools/res_atp.ML Sat Jan 20 14:09:12 2007 +0100
5.2 +++ b/src/HOL/Tools/res_atp.ML Sat Jan 20 14:09:14 2007 +0100
5.3 @@ -56,7 +56,7 @@
5.4 structure ResAtp =
5.5 struct
5.6
5.7 -fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s);
5.8 +fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
5.9
5.10 (********************************************************************)
5.11 (* some settings for both background automatic ATP calling procedure*)
5.12 @@ -237,7 +237,7 @@
5.13 else fn_lg f (FOL,seen)
5.14 in
5.15 if is_fol_logic lg' then ()
5.16 - else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
5.17 + else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
5.18 term_lg (args@tms) (lg',seen')
5.19 end
5.20 | term_lg _ (lg,seen) = (lg,seen)
5.21 @@ -261,7 +261,7 @@
5.22 else pred_lg pred (lg,seen)
5.23 in
5.24 if is_fol_logic lg' then ()
5.25 - else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
5.26 + else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
5.27 term_lg args (lg',seen')
5.28 end;
5.29
5.30 @@ -270,7 +270,7 @@
5.31 let val (lg,seen') = lit_lg lit (FOL,seen)
5.32 in
5.33 if is_fol_logic lg then ()
5.34 - else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
5.35 + else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
5.36 lits_lg lits (lg,seen')
5.37 end
5.38 | lits_lg lits (lg,seen) = (lg,seen);
5.39 @@ -288,7 +288,7 @@
5.40 let val (lg,seen') = logic_of_clause cls (FOL,seen)
5.41 val _ =
5.42 if is_fol_logic lg then ()
5.43 - else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
5.44 + else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
5.45 in
5.46 logic_of_clauses clss (lg,seen')
5.47 end
5.48 @@ -506,7 +506,7 @@
5.49 fun make_unique xs =
5.50 let val ht = mk_clause_table 7000
5.51 in
5.52 - Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses");
5.53 + Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
5.54 app (ignore o Polyhash.peekInsert ht) xs;
5.55 Polyhash.listItems ht
5.56 end;
5.57 @@ -529,7 +529,7 @@
5.58 fun display_thms [] = ()
5.59 | display_thms ((name,thm)::nthms) =
5.60 let val nthm = name ^ ": " ^ (string_of_thm thm)
5.61 - in Output.debug nthm; display_thms nthms end;
5.62 + in Output.debug (fn () => nthm); display_thms nthms end;
5.63
5.64 fun all_valid_thms ctxt =
5.65 PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
5.66 @@ -571,7 +571,7 @@
5.67 let val included_thms =
5.68 if !include_all
5.69 then (tap (fn ths => Output.debug
5.70 - ("Including all " ^ Int.toString (length ths) ^ " theorems"))
5.71 + (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
5.72 (name_thm_pairs ctxt))
5.73 else
5.74 let val claset_thms =
5.75 @@ -583,8 +583,8 @@
5.76 val atpset_thms =
5.77 if !include_atpset then ResAxioms.atpset_rules_of ctxt
5.78 else []
5.79 - val _ = if !Output.show_debug_msgs
5.80 - then (Output.debug "ATP theorems: "; display_thms atpset_thms)
5.81 + val _ = if !Output.debugging
5.82 + then (Output.debug (fn () => "ATP theorems: "); display_thms atpset_thms)
5.83 else ()
5.84 in claset_thms @ simpset_thms @ atpset_thms end
5.85 val user_rules = filter check_named
5.86 @@ -600,12 +600,11 @@
5.87 let val banned = make_banned_test (map #1 ths)
5.88 fun ok (a,_) = not (banned a)
5.89 val (good,bad) = List.partition ok ths
5.90 - in if !Output.show_debug_msgs then
5.91 - (Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
5.92 - Output.debug("filtered: " ^ space_implode ", " (map #1 bad));
5.93 - Output.debug("...and returns " ^ Int.toString (length good)))
5.94 - else ();
5.95 - good
5.96 + in
5.97 + Output.debug (fn () => "blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
5.98 + Output.debug (fn () => "filtered: " ^ space_implode ", " (map #1 bad));
5.99 + Output.debug (fn () => "...and returns " ^ Int.toString (length good));
5.100 + good
5.101 end
5.102 else ths;
5.103
5.104 @@ -751,14 +750,15 @@
5.105 and user_lemmas_names = map #1 user_rules
5.106 in
5.107 writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
5.108 - Output.debug ("Writing to " ^ file);
5.109 + Output.debug (fn () => "Writing to " ^ file);
5.110 file
5.111 end;
5.112
5.113
5.114 (**** remove tmp files ****)
5.115 fun cond_rm_tmp file =
5.116 - if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..."
5.117 + if !Output.debugging orelse !destdir <> ""
5.118 + then Output.debug (fn () => "ATP input kept...")
5.119 else OS.FileSys.remove file;
5.120
5.121
5.122 @@ -785,7 +785,7 @@
5.123 val probfile = prob_pathname n
5.124 val time = Int.toString (!time_limit)
5.125 in
5.126 - Output.debug ("problem file in watcher_call_provers is " ^ probfile);
5.127 + Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
5.128 (*options are separated by Watcher.setting_sep, currently #"%"*)
5.129 if !prover = "spass"
5.130 then
5.131 @@ -816,7 +816,7 @@
5.132 val atp_list = make_atp_list sg_terms 1
5.133 in
5.134 Watcher.callResProvers(childout,atp_list);
5.135 - Output.debug "Sent commands to watcher!"
5.136 + Output.debug (fn () => "Sent commands to watcher!")
5.137 end
5.138
5.139 fun trace_vector fname =
5.140 @@ -829,7 +829,7 @@
5.141 subgoals, each involving &&.*)
5.142 fun write_problem_files probfile (ctxt,th) =
5.143 let val goals = Thm.prems_of th
5.144 - val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
5.145 + val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
5.146 val thy = ProofContext.theory_of ctxt
5.147 fun get_neg_subgoals [] _ = []
5.148 | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
5.149 @@ -844,11 +844,11 @@
5.150 |> ResAxioms.cnf_rules_pairs |> make_unique
5.151 |> restrict_to_logic logic
5.152 |> remove_unwanted_clauses
5.153 - val _ = Output.debug ("included clauses = " ^ Int.toString(length included_cls))
5.154 + val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
5.155 val white_cls = ResAxioms.cnf_rules_pairs white_thms
5.156 (*clauses relevant to goal gl*)
5.157 val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
5.158 - val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
5.159 + val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
5.160 axcls_list
5.161 val writer = if !prover = "spass" then dfg_writer else tptp_writer
5.162 fun write_all [] [] _ = []
5.163 @@ -863,12 +863,12 @@
5.164 and tycons = type_consts_of_terms thy (ccltms@axtms)
5.165 (*TFrees in conjecture clauses; TVars in axiom clauses*)
5.166 val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
5.167 - val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
5.168 + val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
5.169 val arity_clauses = ResClause.arity_clause_thy thy tycons supers
5.170 - val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
5.171 + val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
5.172 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
5.173 val thm_names = Vector.fromList clnames
5.174 - val _ = if !Output.show_debug_msgs
5.175 + val _ = if !Output.debugging
5.176 then trace_vector (fname ^ "_thm_names") thm_names else ()
5.177 in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end
5.178 val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
5.179 @@ -883,10 +883,10 @@
5.180 (case !last_watcher_pid of
5.181 NONE => ()
5.182 | SOME (_, _, pid, files) =>
5.183 - (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
5.184 + (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
5.185 Watcher.killWatcher pid;
5.186 ignore (map (try cond_rm_tmp) files)))
5.187 - handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
5.188 + handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
5.189
5.190 (*writes out the current problems and calls ATPs*)
5.191 fun isar_atp (ctxt, th) =
5.192 @@ -898,8 +898,8 @@
5.193 val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
5.194 in
5.195 last_watcher_pid := SOME (childin, childout, pid, files);
5.196 - Output.debug ("problem files: " ^ space_implode ", " files);
5.197 - Output.debug ("pid: " ^ string_of_pid pid);
5.198 + Output.debug (fn () => "problem files: " ^ space_implode ", " files);
5.199 + Output.debug (fn () => "pid: " ^ string_of_pid pid);
5.200 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
5.201 end;
5.202
5.203 @@ -923,12 +923,12 @@
5.204 fun invoke_atp_ml (ctxt, goal) =
5.205 let val thy = ProofContext.theory_of ctxt;
5.206 in
5.207 - Output.debug ("subgoals in isar_atp:\n" ^
5.208 + Output.debug (fn () => "subgoals in isar_atp:\n" ^
5.209 Pretty.string_of (ProofContext.pretty_term ctxt
5.210 (Logic.mk_conjunction_list (Thm.prems_of goal))));
5.211 - Output.debug ("current theory: " ^ Context.theory_name thy);
5.212 + Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
5.213 inc hook_count;
5.214 - Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
5.215 + Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
5.216 ResClause.init thy;
5.217 ResHolClause.init thy;
5.218 if !time_limit > 0 then isar_atp (ctxt, goal)
6.1 --- a/src/HOL/Tools/res_axioms.ML Sat Jan 20 14:09:12 2007 +0100
6.2 +++ b/src/HOL/Tools/res_axioms.ML Sat Jan 20 14:09:14 2007 +0100
6.3 @@ -467,7 +467,7 @@
6.4 It returns a modified theory, unless skolemization fails.*)
6.5 fun skolem thy (name,th) =
6.6 let val cname = (case name of "" => gensym "" | s => flatten_name s)
6.7 - val _ = Output.debug ("skolemizing " ^ name ^ ": ")
6.8 + val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ")
6.9 in Option.map
6.10 (fn nnfth =>
6.11 let val (thy',defs) = declare_skofuns cname nnfth thy
6.12 @@ -495,28 +495,29 @@
6.13 end)
6.14 | SOME (th',cls) =>
6.15 if eq_thm(th,th') then (cls,thy)
6.16 - else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name);
6.17 - Output.debug (string_of_thm th);
6.18 - Output.debug (string_of_thm th');
6.19 + else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
6.20 + Output.debug (fn () => string_of_thm th);
6.21 + Output.debug (fn () => string_of_thm th');
6.22 ([th],thy));
6.23
6.24 (*Exported function to convert Isabelle theorems into axiom clauses*)
6.25 fun cnf_axiom (name,th) =
6.26 - (Output.debug ("cnf_axiom called, theorem name = " ^ name);
6.27 + (Output.debug (fn () => "cnf_axiom called, theorem name = " ^ name);
6.28 case name of
6.29 "" => skolem_thm th (*no name, so can't cache*)
6.30 | s => case Symtab.lookup (!clause_cache) s of
6.31 NONE =>
6.32 let val cls = map Goal.close_result (skolem_thm th)
6.33 - in Output.debug "inserted into cache";
6.34 + in Output.debug (fn () => "inserted into cache");
6.35 change clause_cache (Symtab.update (s, (th, cls))); cls
6.36 end
6.37 | SOME(th',cls) =>
6.38 if eq_thm(th,th') then cls
6.39 - else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name);
6.40 - Output.debug (string_of_thm th);
6.41 - Output.debug (string_of_thm th');
6.42 - cls)
6.43 + else
6.44 + (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
6.45 + Output.debug (fn () => string_of_thm th);
6.46 + Output.debug (fn () => string_of_thm th');
6.47 + cls)
6.48 );
6.49
6.50 fun pairname th = (PureThy.get_name_hint th, th);
6.51 @@ -533,7 +534,7 @@
6.52 val intros = safeIs @ hazIs
6.53 val elims = map Classical.classical_rule (safeEs @ hazEs)
6.54 in
6.55 - Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^
6.56 + Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^
6.57 " elims: " ^ Int.toString(length elims));
6.58 map pairname (intros @ elims)
6.59 end;
6.60 @@ -542,8 +543,8 @@
6.61 let val ({rules,...}, _) = rep_ss ss
6.62 val simps = Net.entries rules
6.63 in
6.64 - Output.debug ("rules_of_simpset: " ^ Int.toString(length simps));
6.65 - map (fn r => (#name r, #thm r)) simps
6.66 + Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps));
6.67 + map (fn r => (#name r, #thm r)) simps
6.68 end;
6.69
6.70 fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
7.1 --- a/src/HOL/Tools/res_clause.ML Sat Jan 20 14:09:12 2007 +0100
7.2 +++ b/src/HOL/Tools/res_clause.ML Sat Jan 20 14:09:14 2007 +0100
7.3 @@ -425,7 +425,7 @@
7.4 fun make_axiom_clause thm (ax_name,cls_id) =
7.5 if Meson.is_fol_term (prop_of thm)
7.6 then (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE)
7.7 - else (Output.debug ("Omitting " ^ ax_name ^ ": Axiom is not FOL"); NONE)
7.8 + else (Output.debug (fn () => ("Omitting " ^ ax_name ^ ": Axiom is not FOL")); NONE)
7.9
7.10 fun make_axiom_clauses [] = []
7.11 | make_axiom_clauses ((thm,(name,id))::thms) =
7.12 @@ -732,7 +732,7 @@
7.13 (* write out a subgoal in DFG format to the file "xxxx_N"*)
7.14 fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
7.15 let
7.16 - val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
7.17 + val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
7.18 val conjectures = make_conjecture_clauses thms
7.19 val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
7.20 val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
7.21 @@ -818,7 +818,7 @@
7.22 (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
7.23 fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
7.24 let
7.25 - val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
7.26 + val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
7.27 val clss = make_conjecture_clauses thms
7.28 val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
7.29 val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
8.1 --- a/src/HOL/Tools/res_hol_clause.ML Sat Jan 20 14:09:12 2007 +0100
8.2 +++ b/src/HOL/Tools/res_hol_clause.ML Sat Jan 20 14:09:14 2007 +0100
8.3 @@ -536,19 +536,19 @@
8.4 val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
8.5 fun needed c = valOf (Symtab.lookup ct c) > 0
8.6 val IK = if needed "c_COMBI" orelse needed "c_COMBK"
8.7 - then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K])
8.8 + then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
8.9 else []
8.10 val BC = if needed "c_COMBB" orelse needed "c_COMBC"
8.11 - then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C])
8.12 + then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
8.13 else []
8.14 val S = if needed "c_COMBS"
8.15 - then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S])
8.16 + then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
8.17 else []
8.18 val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
8.19 - then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C'])
8.20 + then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
8.21 else []
8.22 val S' = if needed "c_COMBS_e"
8.23 - then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S'])
8.24 + then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
8.25 else []
8.26 val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
8.27 in
8.28 @@ -579,7 +579,7 @@
8.29 fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
8.30
8.31 fun display_arity (c,n) =
8.32 - Output.debug ("Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
8.33 + Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
8.34 (if needs_hBOOL c then " needs hBOOL" else ""));
8.35
8.36 fun count_constants (conjectures, axclauses, helper_clauses) =
9.1 --- a/src/HOL/Tools/res_reconstruct.ML Sat Jan 20 14:09:12 2007 +0100
9.2 +++ b/src/HOL/Tools/res_reconstruct.ML Sat Jan 20 14:09:14 2007 +0100
9.3 @@ -27,7 +27,7 @@
9.4
9.5 val trace_path = Path.basic "atp_trace";
9.6
9.7 -fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
9.8 +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
9.9 else ();
9.10
9.11 (*Full proof reconstruction wanted*)
9.12 @@ -427,11 +427,9 @@
9.13 val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
9.14 val ccls = map forall_intr_vars ccls
9.15 in
9.16 - if !Output.show_debug_msgs
9.17 - then app (Output.debug o string_of_thm) ccls
9.18 - else ();
9.19 - isar_header (map #1 fixes) ^
9.20 - String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
9.21 + app (fn th => Output.debug (fn () => string_of_thm th)) ccls;
9.22 + isar_header (map #1 fixes) ^
9.23 + String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
9.24 end;
9.25
9.26 (*Could use split_lines, but it can return blank lines...*)
10.1 --- a/src/Pure/General/output.ML Sat Jan 20 14:09:12 2007 +0100
10.2 +++ b/src/Pure/General/output.ML Sat Jan 20 14:09:14 2007 +0100
10.3 @@ -27,7 +27,7 @@
10.4 val change_warn: ('b -> 'a -> bool) -> ('a -> 'b -> 'b) -> ('a -> string) -> 'a -> 'b -> 'b
10.5 val update_warn: ('a * 'a -> bool) -> string -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list
10.6 val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
10.7 - val show_debug_msgs: bool ref
10.8 + val debugging: bool ref
10.9 val no_warnings: ('a -> 'b) -> 'a -> 'b
10.10 val timing: bool ref
10.11 val cond_timeit: bool -> (unit -> 'a) -> 'a
10.12 @@ -53,7 +53,7 @@
10.13 val ML_errors: ('a -> 'b) -> 'a -> 'b
10.14 val panic: string -> unit
10.15 val info: string -> unit
10.16 - val debug: string -> unit
10.17 + val debug: (unit -> string) -> unit
10.18 val error_msg: string -> unit
10.19 val ml_output: (string -> unit) * (string -> unit)
10.20 val add_mode: string ->
10.21 @@ -128,8 +128,8 @@
10.22
10.23 fun no_warnings f = setmp warning_fn (K ()) f;
10.24
10.25 -val show_debug_msgs = ref false;
10.26 -fun debug s = if ! show_debug_msgs then ! debug_fn (output s) else ()
10.27 +val debugging = ref false;
10.28 +fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
10.29
10.30 fun error_msg s = ! error_fn (output s);
10.31
11.1 --- a/src/Pure/ProofGeneral/preferences.ML Sat Jan 20 14:09:12 2007 +0100
11.2 +++ b/src/Pure/ProofGeneral/preferences.ML Sat Jan 20 14:09:14 2007 +0100
11.3 @@ -133,9 +133,9 @@
11.4 bool_pref Output.timing
11.5 "global-timing"
11.6 "Whether to enable timing in Isabelle.",
11.7 - bool_pref Output.show_debug_msgs
11.8 - "debug-messages"
11.9 - "Whether to show debugging messages."]
11.10 + bool_pref Toplevel.debug
11.11 + "debugging"
11.12 + "Whether to enable debugging."]
11.13
11.14 val proof_preferences =
11.15 [bool_pref quick_and_dirty