tuned signature -- contrast physical output primitives versus Output.raw_message;

--- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -112,21 +112,21 @@
    ------------------------------------*)
 
 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
-  let fun prec x = (Output.raw_stdout ","; pre x)
+  let fun prec x = (Output.physical_stdout ","; pre x)
   in
     (case lll of
-      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
-    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
+      [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
+    | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
    end;
 
-fun pr_bool true = Output.raw_stdout "true"
-|   pr_bool false = Output.raw_stdout "false";
+fun pr_bool true = Output.physical_stdout "true"
+|   pr_bool false = Output.physical_stdout "false";
 
-fun pr_msg m = Output.raw_stdout "m"
-|   pr_msg n = Output.raw_stdout "n"
-|   pr_msg l = Output.raw_stdout "l";
+fun pr_msg m = Output.physical_stdout "m"
+|   pr_msg n = Output.physical_stdout "n"
+|   pr_msg l = Output.physical_stdout "l";
 
-fun pr_act a = Output.raw_stdout (case a of
+fun pr_act a = Output.physical_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.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
+fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_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.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 "}");
+        (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p;  Output.physical_stdout ", ";
+         pr_bool a;  Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
+         pr_bool b;  Output.physical_stdout ", "; pr_pkt_list ch1;  Output.physical_stdout ", ";
+         pr_bool_list ch2; Output.physical_stdout "}");
 
 
 

--- a/src/Pure/General/output.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/General/output.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -22,9 +22,9 @@
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
-  val raw_stdout: output -> unit
-  val raw_stderr: output -> unit
-  val raw_writeln: output -> unit
+  val physical_stdout: output -> unit
+  val physical_stderr: output -> unit
+  val physical_writeln: output -> unit
   structure Private_Hooks:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -78,24 +78,24 @@
 
 (* raw output primitives -- not to be used in user-space *)
 
-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 physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
-fun raw_writeln "" = ()
-  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
+fun physical_writeln "" = ()
+  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
 
 
 (* Isabelle output channels *)
 
 structure Private_Hooks =
 struct
-  val writeln_fn = Unsynchronized.ref raw_writeln;
+  val writeln_fn = Unsynchronized.ref physical_writeln;
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+  val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
   val error_fn =
-    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
-  val prompt_fn = Unsynchronized.ref raw_stdout;
+    Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
+  val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
   val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -75,7 +75,7 @@
 fun message bg en prfx text =
   (case render text of
     "" => ()
-  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
+  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
  (Output.Private_Hooks.writeln_fn := message "" "" "";
@@ -85,7 +85,7 @@
   Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
   Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -66,7 +66,7 @@
 
 fun matching_pgip_id id = (id = ! pgip_id)
 
-val output_xml_fn = Unsynchronized.ref Output.raw_writeln
+val output_xml_fn = Unsynchronized.ref Output.physical_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;
@@ -1009,7 +1009,7 @@
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local
-    val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
+    val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
 in
 
 (* Set recipient for PGIP results *)

--- a/src/Pure/System/isabelle_process.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -171,7 +171,7 @@
 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
-    val _ = Output.raw_stdout Symbol.STX;
+    val _ = Output.physical_stdout Symbol.STX;
 
     val _ = quick_and_dirty := true;
     val _ = Goal.parallel_proofs := 0;

--- a/src/Pure/System/session.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/System/session.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -107,7 +107,7 @@
           val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
             |> Real.fmt (StringCvt.FIX (SOME 2));
           val _ =
-            Output.raw_stderr ("Timing " ^ item ^ " (" ^
+            Output.physical_stderr ("Timing " ^ item ^ " (" ^
               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
               Timing.message timing ^ ", factor " ^ factor ^ ")\n");
         in () end

--- a/src/Pure/Thy/present.ML	Tue Aug 23 16:41:16 2011 +0200
+++ b/src/Pure/Thy/present.ML	Tue Aug 23 16:53:05 2011 +0200
@@ -289,7 +289,8 @@
       val documents =
         if doc = "" then []
         else if not (can File.check_dir document_path) then
-          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
+          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
+           else (); [])
         else read_variants doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
@@ -403,14 +404,14 @@
         File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
         List.app finish_html thys;
         List.app (uncurry File.write) files;
-        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
         else ())
       else ();
 
     val _ =
       (case dump_prefix of NONE => () | SOME (cp, path) =>
        (prepare_sources cp path;
-        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
+        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
         else ()));
 
     val doc_paths =
@@ -421,7 +422,8 @@
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =
       if verbose then
-        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
+        doc_paths
+        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
       else ();
   in
     browser_info := empty_browser_info;