# HG changeset patch
# User wenzelm
# Date 1285611970 -7200
# Node ID 6d373e9dcb9decff19c473289e3a7c7e170bd5ab
# Parent  4dbc72759706b692424714f34d5d16d3e072a6db
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;

diff -r 4dbc72759706 -r 6d373e9dcb9d src/HOLCF/IOA/ABP/Check.ML
--- a/src/HOLCF/IOA/ABP/Check.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Check.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -112,21 +112,21 @@
    ------------------------------------*)
 
 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
-  let fun prec x = (Output.std_output ","; pre x)
+  let fun prec x = (Output.raw_stdout ","; pre x)
   in
     (case lll of
-      [] => (Output.std_output lpar; Output.std_output rpar)
-    | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
+      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
+    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
    end;
 
-fun pr_bool true = Output.std_output "true"
-|   pr_bool false = Output.std_output "false";
+fun pr_bool true = Output.raw_stdout "true"
+|   pr_bool false = Output.raw_stdout "false";
 
-fun pr_msg m = Output.std_output "m"
-|   pr_msg n = Output.std_output "n"
-|   pr_msg l = Output.std_output "l";
+fun pr_msg m = Output.raw_stdout "m"
+|   pr_msg n = Output.raw_stdout "n"
+|   pr_msg l = Output.raw_stdout "l";
 
-fun pr_act a = Output.std_output (case a of
+fun pr_act a = Output.raw_stdout (case a of
       Next => "Next"|                         
       S_msg(ma) => "S_msg(ma)"  |
       R_msg(ma) => "R_msg(ma)"  |
@@ -135,17 +135,17 @@
       S_ack(b)   => "S_ack(b)" |                      
       R_ack(b)   => "R_ack(b)");
 
-fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
+fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
 
 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) = 
-        (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 "}");
+        (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
+         pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
+         pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
+         pr_bool_list ch2; Output.raw_stdout "}");
 
 
 
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -28,9 +28,9 @@
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
-  val std_output: output -> unit
-  val std_error: output -> unit
-  val writeln_default: output -> unit
+  val raw_stdout: output -> unit
+  val raw_stderr: output -> unit
+  val raw_writeln: output -> unit
   val writeln_fn: (output -> unit) Unsynchronized.ref
   val priority_fn: (output -> unit) Unsynchronized.ref
   val tracing_fn: (output -> unit) Unsynchronized.ref
@@ -77,24 +77,24 @@
 
 (** output channels **)
 
-(* output primitives -- normally NOT used directly!*)
+(* raw output primitives -- not to be used in user-space *)
 
-fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
-fun writeln_default "" = ()
-  | writeln_default s = std_output (suffix "\n" s);
+fun raw_writeln "" = ()
+  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
 
 
 (* Isabelle output channels *)
 
-val writeln_fn = Unsynchronized.ref writeln_default;
+val writeln_fn = Unsynchronized.ref raw_writeln;
 val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
-val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
-val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
-val prompt_fn = Unsynchronized.ref std_output;
+val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = Unsynchronized.ref raw_stdout;
 val status_fn = Unsynchronized.ref (fn _: string => ());
 val report_fn = Unsynchronized.ref (fn _: string => ());
 
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -71,7 +71,7 @@
 fun message bg en prfx text =
   (case render text of
     "" => ()
-  | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
+  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
  (Output.writeln_fn := message "" "" "";
@@ -81,7 +81,7 @@
   Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.warning_fn := message (special "K") (special "L") "### ";
   Output.error_fn := message (special "M") (special "N") "*** ";
-  Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
+  Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -66,7 +66,7 @@
 
 fun matching_pgip_id id = (id = ! pgip_id)
 
-val output_xml_fn = Unsynchronized.ref Output.writeln_default
+val output_xml_fn = Unsynchronized.ref Output.raw_writeln
 fun output_xml s = ! output_xml_fn (XML.string_of s);
 
 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -1032,7 +1032,7 @@
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local
-    val pgip_output_channel = Unsynchronized.ref Output.writeln_default
+    val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
 in
 
 (* Set recipient for PGIP results *)
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -172,7 +172,7 @@
 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
-    val _ = Output.std_output Symbol.STX;
+    val _ = Output.raw_stdout Symbol.STX;
 
     val _ = quick_and_dirty := true;  (* FIXME !? *)
     val _ = Context.set_thread_data NONE;
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/System/session.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -104,7 +104,7 @@
           val _ = use root;
           val stop = end_timing start;
           val _ =
-            Output.std_error ("Timing " ^ item ^ " (" ^
+            Output.raw_stderr ("Timing " ^ item ^ " (" ^
               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
               #message stop ^ ")\n");
         in () end
diff -r 4dbc72759706 -r 6d373e9dcb9d src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Sep 27 18:16:36 2010 +0200
+++ b/src/Pure/Thy/present.ML	Mon Sep 27 20:26:10 2010 +0200
@@ -293,7 +293,7 @@
       val (doc_prefix1, documents) =
         if doc = "" then (NONE, [])
         else if not (File.exists document_path) then
-          (if verbose then Output.std_error "Warning: missing document directory\n" else ();
+          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
             (NONE, []))
         else (SOME (Path.append html_prefix document_path, html_prefix),
           read_versions doc_versions);
@@ -409,12 +409,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 Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
+      if verbose then Output.raw_stderr ("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 Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
+      if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
 
     (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
       documents |> List.app (fn (name, tags) =>
@@ -422,7 +422,7 @@
          val _ = prepare_sources true path;
          val doc_path = isabelle_document true doc_format name tags path result_path;
        in
-         if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
+         if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
        end));
 
     browser_info := empty_browser_info;