# HG changeset patch # User wenzelm # Date 1175638270 -7200 # Node ID d91b4dd651d6c1bfa98ad429ce9c3f67c2845b6b # Parent 6e56ff1a22ebf65798b8f87e4d10a84a797bcd8d cleaned-up Output functions; diff -r 6e56ff1a22eb -r d91b4dd651d6 src/HOL/Tools/refute.ML --- 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 diff -r 6e56ff1a22eb -r d91b4dd651d6 src/HOLCF/IOA/ABP/Check.ML --- 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 "}"); diff -r 6e56ff1a22eb -r d91b4dd651d6 src/Provers/blast.ML --- 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 diff -r 6e56ff1a22eb -r d91b4dd651d6 src/Pure/Thy/present.ML --- 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;