tuned signature -- contrast physical output primitives versus Output.raw_message;
authorwenzelm
Tue Aug 23 16:53:05 2011 +0200 (2011-08-23 ago)
changeset 44389a3b5fdfb04a3
parent 44388 5f9ad3583e0a
child 44426 8d6869a8d4ec
tuned signature -- contrast physical output primitives versus Output.raw_message;
src/HOL/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/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 16:41:16 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 16:53:05 2011 +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.raw_stdout ","; pre x)
     1.8 +  let fun prec x = (Output.physical_stdout ","; pre x)
     1.9    in
    1.10      (case lll of
    1.11 -      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
    1.12 -    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
    1.13 +      [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
    1.14 +    | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
    1.15     end;
    1.16  
    1.17 -fun pr_bool true = Output.raw_stdout "true"
    1.18 -|   pr_bool false = Output.raw_stdout "false";
    1.19 +fun pr_bool true = Output.physical_stdout "true"
    1.20 +|   pr_bool false = Output.physical_stdout "false";
    1.21  
    1.22 -fun pr_msg m = Output.raw_stdout "m"
    1.23 -|   pr_msg n = Output.raw_stdout "n"
    1.24 -|   pr_msg l = Output.raw_stdout "l";
    1.25 +fun pr_msg m = Output.physical_stdout "m"
    1.26 +|   pr_msg n = Output.physical_stdout "n"
    1.27 +|   pr_msg l = Output.physical_stdout "l";
    1.28  
    1.29 -fun pr_act a = Output.raw_stdout (case a of
    1.30 +fun pr_act a = Output.physical_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.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
    1.39 +fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_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.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
    1.47 -         pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
    1.48 -         pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
    1.49 -         pr_bool_list ch2; Output.raw_stdout "}");
    1.50 +        (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p;  Output.physical_stdout ", ";
    1.51 +         pr_bool a;  Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
    1.52 +         pr_bool b;  Output.physical_stdout ", "; pr_pkt_list ch1;  Output.physical_stdout ", ";
    1.53 +         pr_bool_list ch2; Output.physical_stdout "}");
    1.54  
    1.55  
    1.56  
     2.1 --- a/src/Pure/General/output.ML	Tue Aug 23 16:41:16 2011 +0200
     2.2 +++ b/src/Pure/General/output.ML	Tue Aug 23 16:53:05 2011 +0200
     2.3 @@ -22,9 +22,9 @@
     2.4    val output_width: string -> output * int
     2.5    val output: string -> output
     2.6    val escape: output -> string
     2.7 -  val raw_stdout: output -> unit
     2.8 -  val raw_stderr: output -> unit
     2.9 -  val raw_writeln: output -> unit
    2.10 +  val physical_stdout: output -> unit
    2.11 +  val physical_stderr: output -> unit
    2.12 +  val physical_writeln: output -> unit
    2.13    structure Private_Hooks:
    2.14    sig
    2.15      val writeln_fn: (output -> unit) Unsynchronized.ref
    2.16 @@ -78,24 +78,24 @@
    2.17  
    2.18  (* raw output primitives -- not to be used in user-space *)
    2.19  
    2.20 -fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    2.21 -fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    2.22 +fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    2.23 +fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    2.24  
    2.25 -fun raw_writeln "" = ()
    2.26 -  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
    2.27 +fun physical_writeln "" = ()
    2.28 +  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
    2.29  
    2.30  
    2.31  (* Isabelle output channels *)
    2.32  
    2.33  structure Private_Hooks =
    2.34  struct
    2.35 -  val writeln_fn = Unsynchronized.ref raw_writeln;
    2.36 +  val writeln_fn = Unsynchronized.ref physical_writeln;
    2.37    val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.38    val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.39 -  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.40 +  val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
    2.41    val error_fn =
    2.42 -    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
    2.43 -  val prompt_fn = Unsynchronized.ref raw_stdout;
    2.44 +    Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
    2.45 +  val prompt_fn = Unsynchronized.ref physical_stdout;
    2.46    val status_fn = Unsynchronized.ref (fn _: output => ());
    2.47    val report_fn = Unsynchronized.ref (fn _: output => ());
    2.48    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 16:41:16 2011 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 16:53:05 2011 +0200
     3.3 @@ -75,7 +75,7 @@
     3.4  fun message bg en prfx text =
     3.5    (case render text of
     3.6      "" => ()
     3.7 -  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
     3.8 +  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
     3.9  
    3.10  fun setup_messages () =
    3.11   (Output.Private_Hooks.writeln_fn := message "" "" "";
    3.12 @@ -85,7 +85,7 @@
    3.13    Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    3.14    Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
    3.15    Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    3.16 -  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
    3.17 +  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_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	Tue Aug 23 16:41:16 2011 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 16:53:05 2011 +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.raw_writeln
     4.8 +val output_xml_fn = Unsynchronized.ref Output.physical_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 @@ -1009,7 +1009,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.raw_writeln
    4.17 +    val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
    4.18  in
    4.19  
    4.20  (* Set recipient for PGIP results *)
     5.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 23 16:41:16 2011 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 23 16:53:05 2011 +0200
     5.3 @@ -171,7 +171,7 @@
     5.4  fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
     5.5    let
     5.6      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     5.7 -    val _ = Output.raw_stdout Symbol.STX;
     5.8 +    val _ = Output.physical_stdout Symbol.STX;
     5.9  
    5.10      val _ = quick_and_dirty := true;
    5.11      val _ = Goal.parallel_proofs := 0;
     6.1 --- a/src/Pure/System/session.ML	Tue Aug 23 16:41:16 2011 +0200
     6.2 +++ b/src/Pure/System/session.ML	Tue Aug 23 16:53:05 2011 +0200
     6.3 @@ -107,7 +107,7 @@
     6.4            val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
     6.5              |> Real.fmt (StringCvt.FIX (SOME 2));
     6.6            val _ =
     6.7 -            Output.raw_stderr ("Timing " ^ item ^ " (" ^
     6.8 +            Output.physical_stderr ("Timing " ^ item ^ " (" ^
     6.9                string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    6.10                Timing.message timing ^ ", factor " ^ factor ^ ")\n");
    6.11          in () end
     7.1 --- a/src/Pure/Thy/present.ML	Tue Aug 23 16:41:16 2011 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Tue Aug 23 16:53:05 2011 +0200
     7.3 @@ -289,7 +289,8 @@
     7.4        val documents =
     7.5          if doc = "" then []
     7.6          else if not (can File.check_dir document_path) then
     7.7 -          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
     7.8 +          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
     7.9 +           else (); [])
    7.10          else read_variants doc_variants;
    7.11  
    7.12        val parent_index_path = Path.append Path.parent index_path;
    7.13 @@ -403,14 +404,14 @@
    7.14          File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
    7.15          List.app finish_html thys;
    7.16          List.app (uncurry File.write) files;
    7.17 -        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
    7.18 +        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
    7.19          else ())
    7.20        else ();
    7.21  
    7.22      val _ =
    7.23        (case dump_prefix of NONE => () | SOME (cp, path) =>
    7.24         (prepare_sources cp path;
    7.25 -        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
    7.26 +        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
    7.27          else ()));
    7.28  
    7.29      val doc_paths =
    7.30 @@ -421,7 +422,8 @@
    7.31          in isabelle_document true doc_format name tags path html_prefix end);
    7.32      val _ =
    7.33        if verbose then
    7.34 -        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
    7.35 +        doc_paths
    7.36 +        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
    7.37        else ();
    7.38    in
    7.39      browser_info := empty_browser_info;