--- a/src/HOL/Tools/refute.ML Wed Apr 04 00:11:08 2007 +0200
+++ b/src/HOL/Tools/refute.ML Wed Apr 04 00:11:10 2007 +0200
@@ -733,7 +733,7 @@
(* check this. However, getting this really right seems *)
(* difficult because the user may state arbitrary axioms, *)
(* which could interact with overloading to create loops. *)
- ((*immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
+ ((*Output.immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
| NONE => t)
| Free _ => t
| Var _ => t
@@ -772,7 +772,7 @@
fun collect_axioms thy t =
let
- val _ = immediate_output "Adding axioms..."
+ val _ = Output.immediate_output "Adding axioms..."
(* (string * Term.term) list *)
val axioms = Theory.all_axioms_of thy
(* string * Term.term -> Term.term list -> Term.term list *)
@@ -783,7 +783,7 @@
if member (op aconv) axs ax' then
axs
else (
- immediate_output (" " ^ axname);
+ Output.immediate_output (" " ^ axname);
collect_term_axioms (ax' :: axs, ax')
)
end
@@ -1187,7 +1187,7 @@
val init_model = (universe, [])
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1,
bounds = [], wellformed = True}
- val _ = immediate_output ("Translating term (sizes: "
+ val _ = Output.immediate_output ("Translating term (sizes: "
^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
(* translate 'u' and all axioms *)
val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
@@ -1205,20 +1205,20 @@
val fm_ax = PropLogic.all (map toTrue (tl intrs))
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
in
- immediate_output " invoking SAT solver...";
+ Output.immediate_output " invoking SAT solver...";
(case SatSolver.invoke_solver satsolver fm of
SatSolver.SATISFIABLE assignment =>
(writeln " model found!";
writeln ("*** Model found: ***\n" ^ print_model thy model
(fn i => case assignment i of SOME b => b | NONE => true)))
| SatSolver.UNSATISFIABLE _ =>
- (immediate_output " no model exists.\n";
+ (Output.immediate_output " no model exists.\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.")
| SatSolver.UNKNOWN =>
- (immediate_output " no model found.\n";
+ (Output.immediate_output " no model found.\n";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
| NONE => writeln
--- a/src/HOLCF/IOA/ABP/Check.ML Wed Apr 04 00:11:08 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Check.ML Wed Apr 04 00:11:10 2007 +0200
@@ -113,21 +113,21 @@
------------------------------------*)
fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
- let fun prec x = (std_output ","; pre x)
+ let fun prec x = (Output.std_output ","; pre x)
in
(case lll of
- [] => (std_output lpar; std_output rpar)
- | x::lll => (std_output lpar; pre x; List.app prec lll; std_output rpar))
+ [] => (Output.std_output lpar; Output.std_output rpar)
+ | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
end;
-fun pr_bool true = std_output "true"
-| pr_bool false = std_output "false";
+fun pr_bool true = Output.std_output "true"
+| pr_bool false = Output.std_output "false";
-fun pr_msg m = std_output "m"
-| pr_msg n = std_output "n"
-| pr_msg l = std_output "l";
+fun pr_msg m = Output.std_output "m"
+| pr_msg n = Output.std_output "n"
+| pr_msg l = Output.std_output "l";
-fun pr_act a = std_output (case a of
+fun pr_act a = Output.std_output (case a of
Next => "Next"|
S_msg(ma) => "S_msg(ma)" |
R_msg(ma) => "R_msg(ma)" |
@@ -136,17 +136,17 @@
S_ack(b) => "S_ack(b)" |
R_ack(b) => "R_ack(b)");
-fun pr_pkt (b,ma) = (std_output "<"; pr_bool b;std_output ", "; pr_msg ma; std_output ">");
+fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
val pr_bool_list = print_list("[","]",pr_bool);
val pr_msg_list = print_list("[","]",pr_msg);
val pr_pkt_list = print_list("[","]",pr_pkt);
fun pr_tuple (env,p,a,q,b,ch1,ch2) =
- (std_output "{"; pr_bool env; std_output ", "; pr_msg_list p; std_output ", ";
- pr_bool a; std_output ", "; pr_msg_list q; std_output ", ";
- pr_bool b; std_output ", "; pr_pkt_list ch1; std_output ", ";
- pr_bool_list ch2; std_output "}");
+ (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p; Output.std_output ", ";
+ pr_bool a; Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
+ pr_bool b; Output.std_output ", "; pr_pkt_list ch1; Output.std_output ", ";
+ pr_bool_list ch2; Output.std_output "}");
--- 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
--- a/src/Pure/Thy/present.ML Wed Apr 04 00:11:08 2007 +0200
+++ b/src/Pure/Thy/present.ML Wed Apr 04 00:11:10 2007 +0200
@@ -306,7 +306,8 @@
val (doc_prefix1, documents) =
if doc = "" then (NONE, [])
else if not (File.exists document_path) then
- (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, []))
+ (if verbose then Output.std_error "Warning: missing document directory\n" else ();
+ (NONE, []))
else (SOME (Path.append html_prefix document_path, html_prefix),
read_versions doc_versions);
@@ -413,12 +414,12 @@
File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
List.app finish_html thys;
List.app (uncurry File.write) files;
- if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
+ if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
else ();
(case doc_prefix2 of NONE => () | SOME (cp, path) =>
(prepare_sources cp path;
- if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
+ if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
(case doc_prefix1 of NONE => () | SOME (path, result_path) =>
documents |> List.app (fn (name, tags) =>
@@ -426,7 +427,7 @@
val _ = prepare_sources true path;
val doc_path = isatool_document true doc_format name tags path result_path;
in
- if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
+ if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
end));
browser_info := empty_browser_info;