# HG changeset patch # User wenzelm # Date 1087828779 -7200 # Node ID edbc81e6080906c608003541e4147a1e4bb160f5 # Parent 2b5e9b80a8e5fe695c5a1f5b46746a76af71538e immediate_output; diff -r 2b5e9b80a8e5 -r edbc81e60809 src/HOL/Tools/refute.ML --- 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.")) diff -r 2b5e9b80a8e5 -r edbc81e60809 src/Provers/blast.ML --- 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 diff -r 2b5e9b80a8e5 -r edbc81e60809 src/Pure/General/output.ML --- 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);