--- a/src/HOL/Tools/refute.ML Mon Jun 21 16:39:18 2004 +0200
+++ b/src/HOL/Tools/refute.ML Mon Jun 21 16:39:39 2004 +0200
@@ -59,9 +59,6 @@
structure Refute : REFUTE =
struct
- (* FIXME compatibility -- should avoid std_output altogether *)
- val std_output = Output.std_output o Output.output;
-
open PropLogic;
(* We use 'REFUTE' only for internal error conditions that should *)
@@ -408,7 +405,7 @@
fun collect_axioms thy t =
let
- val _ = std_output "Adding axioms..."
+ val _ = immediate_output "Adding axioms..."
(* (string * Term.term) list *)
val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
(* given a constant 's' of type 'T', which is a subterm of 't', where *)
@@ -506,15 +503,15 @@
(* collect relevant type axioms for the argument types *)
foldl collect_type_axioms (axs, Ts)
else
- (std_output (" " ^ axname);
+ (immediate_output (" " ^ axname);
collect_term_axioms (ax :: axs, ax))
| None =>
(* at least collect relevant type axioms for the argument types *)
foldl collect_type_axioms (axs, Ts))
end
(* TODO: include sort axioms *)
- | TFree (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
- | TVar (_, sorts) => ((*if not (null sorts) then std_output " *ignoring sorts*" else ();*) axs)
+ | TFree (_, sorts) => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
+ | TVar (_, sorts) => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
(* Term.term list * Term.term -> Term.term list *)
and collect_term_axioms (axs, t) =
case t of
@@ -535,7 +532,7 @@
if mem_term (ax, axs) then
collect_type_axioms (axs, T)
else
- (std_output " HOL.the_eq_trivial";
+ (immediate_output " HOL.the_eq_trivial";
collect_term_axioms (ax :: axs, ax))
end
| Const ("Hilbert_Choice.Eps", T) =>
@@ -545,7 +542,7 @@
if mem_term (ax, axs) then
collect_type_axioms (axs, T)
else
- (std_output " Hilbert_Choice.someI";
+ (immediate_output " Hilbert_Choice.someI";
collect_term_axioms (ax :: axs, ax))
end
| Const ("All", _) $ t1 => collect_term_axioms (axs, t1)
@@ -638,7 +635,7 @@
(* collect relevant type axioms *)
collect_type_axioms (axs, T)
else
- (std_output (" " ^ axname);
+ (immediate_output (" " ^ axname);
collect_term_axioms (ax :: axs, ax))
| None =>
(* collect relevant type axioms *)
@@ -888,7 +885,7 @@
(let
val init_model = (universe, [])
val init_args = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
- val _ = std_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
+ val _ = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
(* translate 't' and all axioms *)
val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
let
@@ -902,12 +899,12 @@
val fm_ax = PropLogic.all (map toTrue (tl intrs))
val fm = PropLogic.all [#wellformed args, fm_ax, fm_t]
in
- std_output " invoking SAT solver...";
+ immediate_output " invoking SAT solver...";
(case SatSolver.invoke_solver satsolver fm of
SatSolver.SATISFIABLE assignment =>
writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
| _ => (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
- (std_output " no model found.\n";
+ (immediate_output " no model found.\n";
case next_universe universe sizes minsize maxsize of
Some universe' => find_model_loop universe'
| None => writeln "Search terminated, no larger universe within the given limits."))
--- a/src/Provers/blast.ML Mon Jun 21 16:39:18 2004 +0200
+++ b/src/Provers/blast.ML Mon Jun 21 16:39:39 2004 +0200
@@ -627,17 +627,15 @@
end;
-val prs = std_output o Output.output;
-
(*Print tracing information at each iteration of prover*)
fun tracing sign brs =
- let fun printPairs (((G,_)::_,_)::_) = prs(traceTerm sign G)
- | printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
+ let fun printPairs (((G,_)::_,_)::_) = immediate_output(traceTerm sign G)
+ | printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
| printPairs _ = ()
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
(fullTrace := brs0 :: !fullTrace;
- seq (fn _ => prs "+") brs;
- prs (" [" ^ Int.toString lim ^ "] ");
+ seq (fn _ => immediate_output "+") brs;
+ immediate_output (" [" ^ Int.toString lim ^ "] ");
printPairs pairs;
writeln"")
in if !trace then printBrs (map normBr brs) else ()
@@ -650,10 +648,10 @@
if !trace then
(case !ntrail-ntrl of
0 => ()
- | 1 => prs"\t1 variable UPDATED:"
- | n => prs("\t" ^ Int.toString n ^ " variables UPDATED:");
+ | 1 => immediate_output"\t1 variable UPDATED:"
+ | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
- seq (fn v => prs(" " ^ string_of sign 4 (the (!v))))
+ seq (fn v => immediate_output(" " ^ string_of sign 4 (the (!v))))
(List.take(!trail, !ntrail-ntrl));
writeln"")
else ();
@@ -662,9 +660,9 @@
fun traceNew prems =
if !trace then
case length prems of
- 0 => prs"branch closed by rule"
- | 1 => prs"branch extended (1 new subgoal)"
- | n => prs("branch split: "^ Int.toString n ^ " new subgoals")
+ 0 => immediate_output"branch closed by rule"
+ | 1 => immediate_output"branch extended (1 new subgoal)"
+ | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
else ();
@@ -1010,7 +1008,7 @@
None => closeF Ls
| Some tac =>
let val choices' =
- (if !trace then (prs"branch closed";
+ (if !trace then (immediate_output"branch closed";
traceVars sign ntrl)
else ();
prune (nbrs, nxtVars,
@@ -1141,9 +1139,9 @@
clearTo ntrl; raise NEWBRANCHES)
else
traceNew prems;
- if !trace andalso dup then prs" (duplicating)"
+ if !trace andalso dup then immediate_output" (duplicating)"
else ();
- if !trace andalso recur then prs" (recursive)"
+ if !trace andalso recur then immediate_output" (recursive)"
else ();
traceVars sign ntrl;
if null prems then nclosed := !nclosed + 1
--- a/src/Pure/General/output.ML Mon Jun 21 16:39:18 2004 +0200
+++ b/src/Pure/General/output.ML Mon Jun 21 16:39:39 2004 +0200
@@ -11,6 +11,7 @@
val print_mode: string list ref
val std_output: string -> unit
val std_error: string -> unit
+ val immediate_output: string -> unit
val writeln_default: string -> unit
val writeln_fn: (string -> unit) ref
val priority_fn: (string -> unit) ref
@@ -99,13 +100,17 @@
(** output channels **)
-(*primitive process channels -- normally NOT used directly!*)
+(* output primitives -- normally NOT used directly!*)
+
fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+val immediate_output = std_output o output;
val writeln_default = std_output o suffix "\n";
-(*hooks for Isabelle channels*)
+
+(* Isabelle output channels *)
+
val writeln_fn = ref writeln_default;
val priority_fn = ref (fn s => ! writeln_fn s);
val tracing_fn = ref (fn s => ! writeln_fn s);