Output.debug: non-strict;
authorwenzelm
Sat Jan 20 14:09:14 2007 +0100 (2007-01-20)
changeset 221300906fd95e0b5
parent 22129 bb2203c93316
child 22131 fa8960e165a6
Output.debug: non-strict;
renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/Pure/General/output.ML
src/Pure/ProofGeneral/preferences.ML
     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