immediate_output;
authorwenzelm
Mon Jun 21 16:39:39 2004 +0200 (2004-06-21)
changeset 14984edbc81e60809
parent 14983 2b5e9b80a8e5
child 14985 fefcf6cd858a
immediate_output;
src/HOL/Tools/refute.ML
src/Provers/blast.ML
src/Pure/General/output.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Jun 21 16:39:18 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jun 21 16:39:39 2004 +0200
     1.3 @@ -59,9 +59,6 @@
     1.4  structure Refute : REFUTE =
     1.5  struct
     1.6  
     1.7 -	(* FIXME compatibility -- should avoid std_output altogether *)
     1.8 -	val std_output = Output.std_output o Output.output;
     1.9 -
    1.10  	open PropLogic;
    1.11  
    1.12  	(* We use 'REFUTE' only for internal error conditions that should    *)
    1.13 @@ -408,7 +405,7 @@
    1.14  
    1.15  	fun collect_axioms thy t =
    1.16  	let
    1.17 -		val _ = std_output "Adding axioms..."
    1.18 +		val _ = immediate_output "Adding axioms..."
    1.19  		(* (string * Term.term) list *)
    1.20  		val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
    1.21  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.22 @@ -506,15 +503,15 @@
    1.23  								(* collect relevant type axioms for the argument types *)
    1.24  								foldl collect_type_axioms (axs, Ts)
    1.25  							else
    1.26 -								(std_output (" " ^ axname);
    1.27 +								(immediate_output (" " ^ axname);
    1.28  								collect_term_axioms (ax :: axs, ax))
    1.29  						| None =>
    1.30  							(* at least collect relevant type axioms for the argument types *)
    1.31  							foldl collect_type_axioms (axs, Ts))
    1.32  				end
    1.33  			(* TODO: include sort axioms *)
    1.34 -			| TFree (_, sorts)       => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
    1.35 -			| TVar  (_, sorts)       => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
    1.36 +			| TFree (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
    1.37 +			| TVar  (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
    1.38  		(* Term.term list * Term.term -> Term.term list *)
    1.39  		and collect_term_axioms (axs, t) =
    1.40  			case t of
    1.41 @@ -535,7 +532,7 @@
    1.42  					if mem_term (ax, axs) then
    1.43  						collect_type_axioms (axs, T)
    1.44  					else
    1.45 -						(std_output " HOL.the_eq_trivial";
    1.46 +						(immediate_output " HOL.the_eq_trivial";
    1.47  						collect_term_axioms (ax :: axs, ax))
    1.48  				end
    1.49  			| Const ("Hilbert_Choice.Eps", T) =>
    1.50 @@ -545,7 +542,7 @@
    1.51  					if mem_term (ax, axs) then
    1.52  						collect_type_axioms (axs, T)
    1.53  					else
    1.54 -						(std_output " Hilbert_Choice.someI";
    1.55 +						(immediate_output " Hilbert_Choice.someI";
    1.56  						collect_term_axioms (ax :: axs, ax))
    1.57  				end
    1.58  			| Const ("All", _) $ t1           => collect_term_axioms (axs, t1)
    1.59 @@ -638,7 +635,7 @@
    1.60  								(* collect relevant type axioms *)
    1.61  								collect_type_axioms (axs, T)
    1.62  							else
    1.63 -								(std_output (" " ^ axname);
    1.64 +								(immediate_output (" " ^ axname);
    1.65  								collect_term_axioms (ax :: axs, ax))
    1.66  						| None =>
    1.67  							(* collect relevant type axioms *)
    1.68 @@ -888,7 +885,7 @@
    1.69  			(let
    1.70  				val init_model             = (universe, [])
    1.71  				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
    1.72 -				val _                      = std_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.73 +				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.74  				(* translate 't' and all axioms *)
    1.75  				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
    1.76  					let
    1.77 @@ -902,12 +899,12 @@
    1.78  				val fm_ax = PropLogic.all (map toTrue (tl intrs))
    1.79  				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_t]
    1.80  			in
    1.81 -				std_output " invoking SAT solver...";
    1.82 +				immediate_output " invoking SAT solver...";
    1.83  				(case SatSolver.invoke_solver satsolver fm of
    1.84  				  SatSolver.SATISFIABLE assignment =>
    1.85  					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
    1.86  				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
    1.87 -					(std_output " no model found.\n";
    1.88 +					(immediate_output " no model found.\n";
    1.89  					case next_universe universe sizes minsize maxsize of
    1.90  					  Some universe' => find_model_loop universe'
    1.91  					| None           => writeln "Search terminated, no larger universe within the given limits."))
     2.1 --- a/src/Provers/blast.ML	Mon Jun 21 16:39:18 2004 +0200
     2.2 +++ b/src/Provers/blast.ML	Mon Jun 21 16:39:39 2004 +0200
     2.3 @@ -627,17 +627,15 @@
     2.4    end;
     2.5  
     2.6  
     2.7 -val prs = std_output o Output.output;
     2.8 -
     2.9  (*Print tracing information at each iteration of prover*)
    2.10  fun tracing sign brs = 
    2.11 -  let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
    2.12 -	| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
    2.13 +  let fun printPairs (((G,_)::_,_)::_)  = immediate_output(traceTerm sign G)
    2.14 +	| printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
    2.15  	| printPairs _                 = ()
    2.16        fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
    2.17  	    (fullTrace := brs0 :: !fullTrace;
    2.18 -	     seq (fn _ => prs "+") brs;
    2.19 -	     prs (" [" ^ Int.toString lim ^ "] ");
    2.20 +	     seq (fn _ => immediate_output "+") brs;
    2.21 +	     immediate_output (" [" ^ Int.toString lim ^ "] ");
    2.22  	     printPairs pairs;
    2.23  	     writeln"")
    2.24    in if !trace then printBrs (map normBr brs) else ()
    2.25 @@ -650,10 +648,10 @@
    2.26    if !trace then 
    2.27        (case !ntrail-ntrl of
    2.28  	    0 => ()
    2.29 -	  | 1 => prs"\t1 variable UPDATED:"
    2.30 -	  | n => prs("\t" ^ Int.toString n ^ " variables UPDATED:");
    2.31 +	  | 1 => immediate_output"\t1 variable UPDATED:"
    2.32 +	  | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
    2.33         (*display the instantiations themselves, though no variable names*)
    2.34 -       seq (fn v => prs("   " ^ string_of sign 4 (the (!v))))
    2.35 +       seq (fn v => immediate_output("   " ^ string_of sign 4 (the (!v))))
    2.36             (List.take(!trail, !ntrail-ntrl));
    2.37         writeln"")
    2.38      else ();
    2.39 @@ -662,9 +660,9 @@
    2.40  fun traceNew prems =
    2.41      if !trace then 
    2.42          case length prems of
    2.43 -	    0 => prs"branch closed by rule"
    2.44 -	  | 1 => prs"branch extended (1 new subgoal)"
    2.45 -	  | n => prs("branch split: "^ Int.toString n ^ " new subgoals")
    2.46 +	    0 => immediate_output"branch closed by rule"
    2.47 +	  | 1 => immediate_output"branch extended (1 new subgoal)"
    2.48 +	  | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
    2.49      else ();
    2.50  
    2.51  
    2.52 @@ -1010,7 +1008,7 @@
    2.53  			None     => closeF Ls
    2.54  		      | Some tac => 
    2.55  			    let val choices' = 
    2.56 -				    (if !trace then (prs"branch closed";
    2.57 +				    (if !trace then (immediate_output"branch closed";
    2.58  						     traceVars sign ntrl)
    2.59  				               else ();
    2.60  				     prune (nbrs, nxtVars, 
    2.61 @@ -1141,9 +1139,9 @@
    2.62  			    clearTo ntrl;  raise NEWBRANCHES)
    2.63  		       else 
    2.64  			 traceNew prems;  
    2.65 -			 if !trace andalso dup then prs" (duplicating)"
    2.66 +			 if !trace andalso dup then immediate_output" (duplicating)"
    2.67  					         else ();
    2.68 -			 if !trace andalso recur then prs" (recursive)"
    2.69 +			 if !trace andalso recur then immediate_output" (recursive)"
    2.70  					         else ();
    2.71  			 traceVars sign ntrl;
    2.72  			 if null prems then nclosed := !nclosed + 1
     3.1 --- a/src/Pure/General/output.ML	Mon Jun 21 16:39:18 2004 +0200
     3.2 +++ b/src/Pure/General/output.ML	Mon Jun 21 16:39:39 2004 +0200
     3.3 @@ -11,6 +11,7 @@
     3.4    val print_mode: string list ref
     3.5    val std_output: string -> unit
     3.6    val std_error: string -> unit
     3.7 +  val immediate_output: string -> unit
     3.8    val writeln_default: string -> unit
     3.9    val writeln_fn: (string -> unit) ref
    3.10    val priority_fn: (string -> unit) ref
    3.11 @@ -99,13 +100,17 @@
    3.12  
    3.13  (** output channels **)
    3.14  
    3.15 -(*primitive process channels -- normally NOT used directly!*)
    3.16 +(* output primitives -- normally NOT used directly!*)
    3.17 +
    3.18  fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    3.19  fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    3.20  
    3.21 +val immediate_output = std_output o output;
    3.22  val writeln_default = std_output o suffix "\n";
    3.23  
    3.24 -(*hooks for Isabelle channels*)
    3.25 +
    3.26 +(* Isabelle output channels *)
    3.27 +
    3.28  val writeln_fn = ref writeln_default;
    3.29  val priority_fn = ref (fn s => ! writeln_fn s);
    3.30  val tracing_fn = ref (fn s => ! writeln_fn s);