cleaned-up Output functions;
authorwenzelm
Wed Apr 04 00:11:10 2007 +0200 (2007-04-04 ago)
changeset 22580d91b4dd651d6
parent 22579 6e56ff1a22eb
child 22581 0a995d40160a
cleaned-up Output functions;
src/HOL/Tools/refute.ML
src/HOLCF/IOA/ABP/Check.ML
src/Provers/blast.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Apr 04 00:11:08 2007 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Apr 04 00:11:10 2007 +0200
     1.3 @@ -733,7 +733,7 @@
     1.4            (* check this.  However, getting this really right seems   *)
     1.5            (* difficult because the user may state arbitrary axioms,  *)
     1.6            (* which could interact with overloading to create loops.  *)
     1.7 -          ((*immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
     1.8 +          ((*Output.immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
     1.9          | NONE => t)
    1.10        | Free _           => t
    1.11        | Var _            => t
    1.12 @@ -772,7 +772,7 @@
    1.13  
    1.14    fun collect_axioms thy t =
    1.15    let
    1.16 -    val _ = immediate_output "Adding axioms..."
    1.17 +    val _ = Output.immediate_output "Adding axioms..."
    1.18      (* (string * Term.term) list *)
    1.19      val axioms = Theory.all_axioms_of thy
    1.20      (* string * Term.term -> Term.term list -> Term.term list *)
    1.21 @@ -783,7 +783,7 @@
    1.22        if member (op aconv) axs ax' then
    1.23          axs
    1.24        else (
    1.25 -        immediate_output (" " ^ axname);
    1.26 +        Output.immediate_output (" " ^ axname);
    1.27          collect_term_axioms (ax' :: axs, ax')
    1.28        )
    1.29      end
    1.30 @@ -1187,7 +1187,7 @@
    1.31          val init_model = (universe, [])
    1.32          val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
    1.33            bounds = [], wellformed = True}
    1.34 -        val _          = immediate_output ("Translating term (sizes: "
    1.35 +        val _          = Output.immediate_output ("Translating term (sizes: "
    1.36            ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
    1.37          (* translate 'u' and all axioms *)
    1.38          val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
    1.39 @@ -1205,20 +1205,20 @@
    1.40          val fm_ax = PropLogic.all (map toTrue (tl intrs))
    1.41          val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
    1.42        in
    1.43 -        immediate_output " invoking SAT solver...";
    1.44 +        Output.immediate_output " invoking SAT solver...";
    1.45          (case SatSolver.invoke_solver satsolver fm of
    1.46            SatSolver.SATISFIABLE assignment =>
    1.47            (writeln " model found!";
    1.48            writeln ("*** Model found: ***\n" ^ print_model thy model
    1.49              (fn i => case assignment i of SOME b => b | NONE => true)))
    1.50          | SatSolver.UNSATISFIABLE _ =>
    1.51 -          (immediate_output " no model exists.\n";
    1.52 +          (Output.immediate_output " no model exists.\n";
    1.53            case next_universe universe sizes minsize maxsize of
    1.54              SOME universe' => find_model_loop universe'
    1.55            | NONE           => writeln
    1.56              "Search terminated, no larger universe within the given limits.")
    1.57          | SatSolver.UNKNOWN =>
    1.58 -          (immediate_output " no model found.\n";
    1.59 +          (Output.immediate_output " no model found.\n";
    1.60            case next_universe universe sizes minsize maxsize of
    1.61              SOME universe' => find_model_loop universe'
    1.62            | NONE           => writeln
     2.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Wed Apr 04 00:11:08 2007 +0200
     2.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed Apr 04 00:11:10 2007 +0200
     2.3 @@ -113,21 +113,21 @@
     2.4     ------------------------------------*)
     2.5  
     2.6  fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
     2.7 -  let fun prec x = (std_output ","; pre x)
     2.8 +  let fun prec x = (Output.std_output ","; pre x)
     2.9    in
    2.10      (case lll of
    2.11 -      [] => (std_output lpar; std_output rpar)
    2.12 -    | x::lll => (std_output lpar; pre x; List.app prec lll; std_output rpar))
    2.13 +      [] => (Output.std_output lpar; Output.std_output rpar)
    2.14 +    | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
    2.15     end;
    2.16  
    2.17 -fun pr_bool true = std_output "true"
    2.18 -|   pr_bool false = std_output "false";
    2.19 +fun pr_bool true = Output.std_output "true"
    2.20 +|   pr_bool false = Output.std_output "false";
    2.21  
    2.22 -fun pr_msg m = std_output "m"
    2.23 -|   pr_msg n = std_output "n"
    2.24 -|   pr_msg l = std_output "l";
    2.25 +fun pr_msg m = Output.std_output "m"
    2.26 +|   pr_msg n = Output.std_output "n"
    2.27 +|   pr_msg l = Output.std_output "l";
    2.28  
    2.29 -fun pr_act a = std_output (case a of
    2.30 +fun pr_act a = Output.std_output (case a of
    2.31        Next => "Next"|                         
    2.32        S_msg(ma) => "S_msg(ma)"  |
    2.33        R_msg(ma) => "R_msg(ma)"  |
    2.34 @@ -136,17 +136,17 @@
    2.35        S_ack(b)   => "S_ack(b)" |                      
    2.36        R_ack(b)   => "R_ack(b)");
    2.37  
    2.38 -fun pr_pkt (b,ma) = (std_output "<"; pr_bool b;std_output ", "; pr_msg ma; std_output ">");
    2.39 +fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
    2.40  
    2.41  val pr_bool_list  = print_list("[","]",pr_bool);
    2.42  val pr_msg_list   = print_list("[","]",pr_msg);
    2.43  val pr_pkt_list   = print_list("[","]",pr_pkt);
    2.44  
    2.45  fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
    2.46 -        (std_output "{"; pr_bool env; std_output ", "; pr_msg_list p;  std_output ", ";
    2.47 -         pr_bool a;  std_output ", "; pr_msg_list q; std_output ", ";
    2.48 -         pr_bool b;  std_output ", "; pr_pkt_list ch1;  std_output ", ";
    2.49 -         pr_bool_list ch2; std_output "}");
    2.50 +        (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p;  Output.std_output ", ";
    2.51 +         pr_bool a;  Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
    2.52 +         pr_bool b;  Output.std_output ", "; pr_pkt_list ch1;  Output.std_output ", ";
    2.53 +         pr_bool_list ch2; Output.std_output "}");
    2.54  
    2.55  
    2.56  
     3.1 --- a/src/Provers/blast.ML	Wed Apr 04 00:11:08 2007 +0200
     3.2 +++ b/src/Provers/blast.ML	Wed Apr 04 00:11:10 2007 +0200
     3.3 @@ -628,13 +628,13 @@
     3.4  
     3.5  (*Print tracing information at each iteration of prover*)
     3.6  fun tracing sign brs =
     3.7 -  let fun printPairs (((G,_)::_,_)::_)  = immediate_output(traceTerm sign G)
     3.8 -        | printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
     3.9 +  let fun printPairs (((G,_)::_,_)::_)  = Output.immediate_output(traceTerm sign G)
    3.10 +        | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm sign H ^ "\t (Unsafe)")
    3.11          | printPairs _                 = ()
    3.12        fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
    3.13              (fullTrace := brs0 :: !fullTrace;
    3.14 -             List.app (fn _ => immediate_output "+") brs;
    3.15 -             immediate_output (" [" ^ Int.toString lim ^ "] ");
    3.16 +             List.app (fn _ => Output.immediate_output "+") brs;
    3.17 +             Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
    3.18               printPairs pairs;
    3.19               writeln"")
    3.20    in if !trace then printBrs (map normBr brs) else ()
    3.21 @@ -647,10 +647,10 @@
    3.22    if !trace then
    3.23        (case !ntrail-ntrl of
    3.24              0 => ()
    3.25 -          | 1 => immediate_output"\t1 variable UPDATED:"
    3.26 -          | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
    3.27 +          | 1 => Output.immediate_output"\t1 variable UPDATED:"
    3.28 +          | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
    3.29         (*display the instantiations themselves, though no variable names*)
    3.30 -       List.app (fn v => immediate_output("   " ^ string_of sign 4 (the (!v))))
    3.31 +       List.app (fn v => Output.immediate_output("   " ^ string_of sign 4 (the (!v))))
    3.32             (List.take(!trail, !ntrail-ntrl));
    3.33         writeln"")
    3.34      else ();
    3.35 @@ -659,9 +659,9 @@
    3.36  fun traceNew prems =
    3.37      if !trace then
    3.38          case length prems of
    3.39 -            0 => immediate_output"branch closed by rule"
    3.40 -          | 1 => immediate_output"branch extended (1 new subgoal)"
    3.41 -          | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
    3.42 +            0 => Output.immediate_output"branch closed by rule"
    3.43 +          | 1 => Output.immediate_output"branch extended (1 new subgoal)"
    3.44 +          | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
    3.45      else ();
    3.46  
    3.47  
    3.48 @@ -994,7 +994,7 @@
    3.49                          NONE     => closeF Ls
    3.50                        | SOME tac =>
    3.51                              let val choices' =
    3.52 -                                    (if !trace then (immediate_output"branch closed";
    3.53 +                                    (if !trace then (Output.immediate_output"branch closed";
    3.54                                                       traceVars sign ntrl)
    3.55                                                 else ();
    3.56                                       prune (nbrs, nxtVars,
    3.57 @@ -1125,9 +1125,9 @@
    3.58                              clearTo ntrl;  raise NEWBRANCHES)
    3.59                         else
    3.60                           traceNew prems;
    3.61 -                         if !trace andalso dup then immediate_output" (duplicating)"
    3.62 +                         if !trace andalso dup then Output.immediate_output" (duplicating)"
    3.63                                                   else ();
    3.64 -                         if !trace andalso recur then immediate_output" (recursive)"
    3.65 +                         if !trace andalso recur then Output.immediate_output" (recursive)"
    3.66                                                   else ();
    3.67                           traceVars sign ntrl;
    3.68                           if null prems then nclosed := !nclosed + 1
     4.1 --- a/src/Pure/Thy/present.ML	Wed Apr 04 00:11:08 2007 +0200
     4.2 +++ b/src/Pure/Thy/present.ML	Wed Apr 04 00:11:10 2007 +0200
     4.3 @@ -306,7 +306,8 @@
     4.4        val (doc_prefix1, documents) =
     4.5          if doc = "" then (NONE, [])
     4.6          else if not (File.exists document_path) then
     4.7 -          (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, []))
     4.8 +          (if verbose then Output.std_error "Warning: missing document directory\n" else ();
     4.9 +            (NONE, []))
    4.10          else (SOME (Path.append html_prefix document_path, html_prefix),
    4.11            read_versions doc_versions);
    4.12  
    4.13 @@ -413,12 +414,12 @@
    4.14        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
    4.15        List.app finish_html thys;
    4.16        List.app (uncurry File.write) files;
    4.17 -      if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
    4.18 +      if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
    4.19      else ();
    4.20  
    4.21      (case doc_prefix2 of NONE => () | SOME (cp, path) =>
    4.22       (prepare_sources cp path;
    4.23 -      if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
    4.24 +      if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
    4.25  
    4.26      (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
    4.27        documents |> List.app (fn (name, tags) =>
    4.28 @@ -426,7 +427,7 @@
    4.29           val _ = prepare_sources true path;
    4.30           val doc_path = isatool_document true doc_format name tags path result_path;
    4.31         in
    4.32 -         if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
    4.33 +         if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
    4.34         end));
    4.35  
    4.36      browser_info := empty_browser_info;