renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
authorwenzelm
Mon Sep 27 20:26:10 2010 +0200 (2010-09-27 ago)
changeset 397336d373e9dcb9d
parent 39732 4dbc72759706
child 39734 47f5a8c92666
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
src/HOLCF/IOA/ABP/Check.ML
src/Pure/General/output.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Mon Sep 27 18:16:36 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Mon Sep 27 20:26:10 2010 +0200
     1.3 @@ -112,21 +112,21 @@
     1.4     ------------------------------------*)
     1.5  
     1.6  fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
     1.7 -  let fun prec x = (Output.std_output ","; pre x)
     1.8 +  let fun prec x = (Output.raw_stdout ","; pre x)
     1.9    in
    1.10      (case lll of
    1.11 -      [] => (Output.std_output lpar; Output.std_output rpar)
    1.12 -    | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
    1.13 +      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
    1.14 +    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
    1.15     end;
    1.16  
    1.17 -fun pr_bool true = Output.std_output "true"
    1.18 -|   pr_bool false = Output.std_output "false";
    1.19 +fun pr_bool true = Output.raw_stdout "true"
    1.20 +|   pr_bool false = Output.raw_stdout "false";
    1.21  
    1.22 -fun pr_msg m = Output.std_output "m"
    1.23 -|   pr_msg n = Output.std_output "n"
    1.24 -|   pr_msg l = Output.std_output "l";
    1.25 +fun pr_msg m = Output.raw_stdout "m"
    1.26 +|   pr_msg n = Output.raw_stdout "n"
    1.27 +|   pr_msg l = Output.raw_stdout "l";
    1.28  
    1.29 -fun pr_act a = Output.std_output (case a of
    1.30 +fun pr_act a = Output.raw_stdout (case a of
    1.31        Next => "Next"|                         
    1.32        S_msg(ma) => "S_msg(ma)"  |
    1.33        R_msg(ma) => "R_msg(ma)"  |
    1.34 @@ -135,17 +135,17 @@
    1.35        S_ack(b)   => "S_ack(b)" |                      
    1.36        R_ack(b)   => "R_ack(b)");
    1.37  
    1.38 -fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
    1.39 +fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
    1.40  
    1.41  val pr_bool_list  = print_list("[","]",pr_bool);
    1.42  val pr_msg_list   = print_list("[","]",pr_msg);
    1.43  val pr_pkt_list   = print_list("[","]",pr_pkt);
    1.44  
    1.45  fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
    1.46 -        (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p;  Output.std_output ", ";
    1.47 -         pr_bool a;  Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
    1.48 -         pr_bool b;  Output.std_output ", "; pr_pkt_list ch1;  Output.std_output ", ";
    1.49 -         pr_bool_list ch2; Output.std_output "}");
    1.50 +        (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
    1.51 +         pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
    1.52 +         pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
    1.53 +         pr_bool_list ch2; Output.raw_stdout "}");
    1.54  
    1.55  
    1.56  
     2.1 --- a/src/Pure/General/output.ML	Mon Sep 27 18:16:36 2010 +0200
     2.2 +++ b/src/Pure/General/output.ML	Mon Sep 27 20:26:10 2010 +0200
     2.3 @@ -28,9 +28,9 @@
     2.4    val output_width: string -> output * int
     2.5    val output: string -> output
     2.6    val escape: output -> string
     2.7 -  val std_output: output -> unit
     2.8 -  val std_error: output -> unit
     2.9 -  val writeln_default: output -> unit
    2.10 +  val raw_stdout: output -> unit
    2.11 +  val raw_stderr: output -> unit
    2.12 +  val raw_writeln: output -> unit
    2.13    val writeln_fn: (output -> unit) Unsynchronized.ref
    2.14    val priority_fn: (output -> unit) Unsynchronized.ref
    2.15    val tracing_fn: (output -> unit) Unsynchronized.ref
    2.16 @@ -77,24 +77,24 @@
    2.17  
    2.18  (** output channels **)
    2.19  
    2.20 -(* output primitives -- normally NOT used directly!*)
    2.21 +(* raw output primitives -- not to be used in user-space *)
    2.22  
    2.23 -fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    2.24 -fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    2.25 +fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    2.26 +fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    2.27  
    2.28 -fun writeln_default "" = ()
    2.29 -  | writeln_default s = std_output (suffix "\n" s);
    2.30 +fun raw_writeln "" = ()
    2.31 +  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
    2.32  
    2.33  
    2.34  (* Isabelle output channels *)
    2.35  
    2.36 -val writeln_fn = Unsynchronized.ref writeln_default;
    2.37 +val writeln_fn = Unsynchronized.ref raw_writeln;
    2.38  val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.39  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.40 -val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
    2.41 -val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
    2.42 -val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
    2.43 -val prompt_fn = Unsynchronized.ref std_output;
    2.44 +val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.45 +val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    2.46 +val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
    2.47 +val prompt_fn = Unsynchronized.ref raw_stdout;
    2.48  val status_fn = Unsynchronized.ref (fn _: string => ());
    2.49  val report_fn = Unsynchronized.ref (fn _: string => ());
    2.50  
     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Sep 27 18:16:36 2010 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Sep 27 20:26:10 2010 +0200
     3.3 @@ -71,7 +71,7 @@
     3.4  fun message bg en prfx text =
     3.5    (case render text of
     3.6      "" => ()
     3.7 -  | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
     3.8 +  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
     3.9  
    3.10  fun setup_messages () =
    3.11   (Output.writeln_fn := message "" "" "";
    3.12 @@ -81,7 +81,7 @@
    3.13    Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    3.14    Output.warning_fn := message (special "K") (special "L") "### ";
    3.15    Output.error_fn := message (special "M") (special "N") "*** ";
    3.16 -  Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
    3.17 +  Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
    3.18  
    3.19  fun panic s =
    3.20    (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 27 18:16:36 2010 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 27 20:26:10 2010 +0200
     4.3 @@ -66,7 +66,7 @@
     4.4  
     4.5  fun matching_pgip_id id = (id = ! pgip_id)
     4.6  
     4.7 -val output_xml_fn = Unsynchronized.ref Output.writeln_default
     4.8 +val output_xml_fn = Unsynchronized.ref Output.raw_writeln
     4.9  fun output_xml s = ! output_xml_fn (XML.string_of s);
    4.10  
    4.11  val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    4.12 @@ -1032,7 +1032,7 @@
    4.13  (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
    4.14  
    4.15  local
    4.16 -    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
    4.17 +    val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
    4.18  in
    4.19  
    4.20  (* Set recipient for PGIP results *)
     5.1 --- a/src/Pure/System/isabelle_process.ML	Mon Sep 27 18:16:36 2010 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Sep 27 20:26:10 2010 +0200
     5.3 @@ -172,7 +172,7 @@
     5.4  fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
     5.5    let
     5.6      val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
     5.7 -    val _ = Output.std_output Symbol.STX;
     5.8 +    val _ = Output.raw_stdout Symbol.STX;
     5.9  
    5.10      val _ = quick_and_dirty := true;  (* FIXME !? *)
    5.11      val _ = Context.set_thread_data NONE;
     6.1 --- a/src/Pure/System/session.ML	Mon Sep 27 18:16:36 2010 +0200
     6.2 +++ b/src/Pure/System/session.ML	Mon Sep 27 20:26:10 2010 +0200
     6.3 @@ -104,7 +104,7 @@
     6.4            val _ = use root;
     6.5            val stop = end_timing start;
     6.6            val _ =
     6.7 -            Output.std_error ("Timing " ^ item ^ " (" ^
     6.8 +            Output.raw_stderr ("Timing " ^ item ^ " (" ^
     6.9                string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    6.10                #message stop ^ ")\n");
    6.11          in () end
     7.1 --- a/src/Pure/Thy/present.ML	Mon Sep 27 18:16:36 2010 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Mon Sep 27 20:26:10 2010 +0200
     7.3 @@ -293,7 +293,7 @@
     7.4        val (doc_prefix1, documents) =
     7.5          if doc = "" then (NONE, [])
     7.6          else if not (File.exists document_path) then
     7.7 -          (if verbose then Output.std_error "Warning: missing document directory\n" else ();
     7.8 +          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
     7.9              (NONE, []))
    7.10          else (SOME (Path.append html_prefix document_path, html_prefix),
    7.11            read_versions doc_versions);
    7.12 @@ -409,12 +409,12 @@
    7.13        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
    7.14        List.app finish_html thys;
    7.15        List.app (uncurry File.write) files;
    7.16 -      if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
    7.17 +      if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
    7.18      else ();
    7.19  
    7.20      (case doc_prefix2 of NONE => () | SOME (cp, path) =>
    7.21       (prepare_sources cp path;
    7.22 -      if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
    7.23 +      if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
    7.24  
    7.25      (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
    7.26        documents |> List.app (fn (name, tags) =>
    7.27 @@ -422,7 +422,7 @@
    7.28           val _ = prepare_sources true path;
    7.29           val doc_path = isabelle_document true doc_format name tags path result_path;
    7.30         in
    7.31 -         if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
    7.32 +         if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
    7.33         end));
    7.34  
    7.35      browser_info := empty_browser_info;