--- a/src/Pure/search.ML Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/search.ML Wed Nov 25 13:57:44 1998 +0100
@@ -225,12 +225,12 @@
(case partition satpred prfs of
([],[]) => []
| ([],nonsats) =>
- (message("breadth=" ^ string_of_int(length nonsats) ^ "\n");
+ (message("breadth=" ^ string_of_int(length nonsats));
bfs (List.concat (map tacf nonsats)))
| (sats,_) => sats)
in (fn st => Seq.of_list (bfs [st])) end;
-val BREADTH_FIRST = gen_BREADTH_FIRST prs;
+val BREADTH_FIRST = gen_BREADTH_FIRST writeln;
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
--- a/src/Pure/tactic.ML Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/tactic.ML Wed Nov 25 13:57:44 1998 +0100
@@ -102,7 +102,7 @@
fun trace_goalno_tac tac i st =
case Seq.pull(tac i st) of
None => Seq.empty
- | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n");
+ | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected");
Seq.make(fn()=> seqcell));
--- a/src/Pure/tctical.ML Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/tctical.ML Wed Nov 25 13:57:44 1998 +0100
@@ -198,9 +198,9 @@
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
- (prs"** Press RETURN to continue: ";
+ (writeln "** Press RETURN to continue: ";
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
- else (prs"Goodbye\n"; Seq.empty));
+ else (writeln "Goodbye"; Seq.empty));
exception TRACE_EXIT of thm
and TRACE_QUIT;
@@ -216,9 +216,9 @@
| "f\n" => Seq.empty
| "o\n" => (flag:=false; tac st)
| "s\n" => (suppress_tracing:=true; tac st)
- | "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT st))
+ | "x\n" => (writeln "Exiting now"; raise (TRACE_EXIT st))
| "quit\n" => raise TRACE_QUIT
- | _ => (prs
+ | _ => (writeln
"Type RETURN to continue or...\n\
\ f - to fail here\n\
\ o - to switch tracing off\n\
@@ -232,7 +232,7 @@
fun tracify flag tac st =
if !flag andalso not (!suppress_tracing)
then (print_goals (!goals_limit) st;
- prs"** Press RETURN to continue: ";
+ writeln "** Press RETURN to continue: ";
exec_trace_command flag (tac,st))
else tac st;