--- a/src/Provers/blast.ML Wed Apr 04 00:11:08 2007 +0200
+++ b/src/Provers/blast.ML Wed Apr 04 00:11:10 2007 +0200
@@ -628,13 +628,13 @@
(*Print tracing information at each iteration of prover*)
fun tracing sign brs =
- let fun printPairs (((G,_)::_,_)::_) = immediate_output(traceTerm sign G)
- | printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
+ let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm sign G)
+ | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm sign H ^ "\t (Unsafe)")
| printPairs _ = ()
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
(fullTrace := brs0 :: !fullTrace;
- List.app (fn _ => immediate_output "+") brs;
- immediate_output (" [" ^ Int.toString lim ^ "] ");
+ List.app (fn _ => Output.immediate_output "+") brs;
+ Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
printPairs pairs;
writeln"")
in if !trace then printBrs (map normBr brs) else ()
@@ -647,10 +647,10 @@
if !trace then
(case !ntrail-ntrl of
0 => ()
- | 1 => immediate_output"\t1 variable UPDATED:"
- | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
+ | 1 => Output.immediate_output"\t1 variable UPDATED:"
+ | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
- List.app (fn v => immediate_output(" " ^ string_of sign 4 (the (!v))))
+ List.app (fn v => Output.immediate_output(" " ^ string_of sign 4 (the (!v))))
(List.take(!trail, !ntrail-ntrl));
writeln"")
else ();
@@ -659,9 +659,9 @@
fun traceNew prems =
if !trace then
case length prems of
- 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")
+ 0 => Output.immediate_output"branch closed by rule"
+ | 1 => Output.immediate_output"branch extended (1 new subgoal)"
+ | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
else ();
@@ -994,7 +994,7 @@
NONE => closeF Ls
| SOME tac =>
let val choices' =
- (if !trace then (immediate_output"branch closed";
+ (if !trace then (Output.immediate_output"branch closed";
traceVars sign ntrl)
else ();
prune (nbrs, nxtVars,
@@ -1125,9 +1125,9 @@
clearTo ntrl; raise NEWBRANCHES)
else
traceNew prems;
- if !trace andalso dup then immediate_output" (duplicating)"
+ if !trace andalso dup then Output.immediate_output" (duplicating)"
else ();
- if !trace andalso recur then immediate_output" (recursive)"
+ if !trace andalso recur then Output.immediate_output" (recursive)"
else ();
traceVars sign ntrl;
if null prems then nclosed := !nclosed + 1