src/HOL/Tools/res_atp.ML

 end;
 
 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*)
 (* and also explicit ATP invocation methods                         *)
 (********************************************************************)

       let val (f,args) = strip_comb tm
           val (lg',seen') = if f mem seen then (FOL,seen)
                             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)
 
 exception PRED_LG of term;

       let val (pred,args) = strip_comb P
           val (lg',seen') = if pred mem seen then (lg,seen)
                             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;
 
 fun lits_lg [] (lg,seen) = (lg,seen)
   | lits_lg (lit::lits) (FOL,seen) =
       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);
 
 fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs

 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   | logic_of_clauses (cls::clss) (FOL,seen) =
     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
   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
 

 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
 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;
 
 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically

   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
 
 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) ([], []) @
   filter (ProofContext.valid_thms ctxt)
     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));

 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
 fun get_clasimp_atp_lemmas ctxt user_thms =
   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 =
                 if !include_claset then ResAxioms.claset_rules_of ctxt
                 else []

                 if !include_simpset then ResAxioms.simpset_rules_of ctxt
                 else []
             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
                          (map (ResAxioms.pairname)
                            (if null user_thms then !whitelist else user_thms))

 fun blacklist_filter ths =
   if !run_blacklist_filter then
       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;
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)

         val writer = if dfg then dfg_writer else tptp_writer
         and file = atp_input_file()
         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;
 
 
 (****** setup ATPs as Isabelle methods ******)
 

       | make_atp_list (sg_term::xs) n =
           let
             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
               let val spass = helper_path "SPASS_HOME" "SPASS"
                   val sopts =

           end
 
     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 =
   let val path = File.explode_platform_path fname
   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;

   and allows the suppression of the suffix "_1" in problem-generation mode.
   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   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) :: 
                                          get_neg_subgoals gls (n+1)
       val goal_cls = get_neg_subgoals goals 1

       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
       val included_cls = included_thms |> blacklist_filter
                                        |> 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 [] [] _ = []
         | write_all (ccls::ccls_list) (axcls::axcls_list) k =
             let val fname = probfile k

                 val subs = tfree_classes_of_terms ccltms
                 and supers = tvar_classes_of_terms axtms
                 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)
   in
       (filenames, thm_names_list)

 
 fun kill_last_watcher () =
     (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) =
   if Thm.no_prems th then ()
   else

       val _ = kill_last_watcher()
       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
       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;
 
 (*For ML scripts, and primarily, for debugging*)
 fun callatp () =

 (** the Isar toplevel hook **)
 
 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)
     else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
   end;