export writeln_default;
authorwenzelm
Sat Dec 08 14:42:03 2001 +0100 (2001-12-08)
changeset 124196a7ee57447aa
parent 12418 753054ec8e88
child 12420 a2a05c952b4d
export writeln_default;
tuned prefix_lines;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Dec 08 14:41:36 2001 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Dec 08 14:42:03 2001 +0100
     1.3 @@ -159,6 +159,7 @@
     1.4    val space_explode: string -> string -> string list
     1.5    val std_output: string -> unit
     1.6    val std_error: string -> unit
     1.7 +  val writeln_default: string -> unit
     1.8    val prefix_lines: string -> string -> string
     1.9    val split_lines: string -> string list
    1.10    val untabify: string list -> string list
    1.11 @@ -1139,11 +1140,13 @@
    1.12  fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.13  fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    1.14  
    1.15 -fun prefix_lines prfx txt =
    1.16 -  txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
    1.17 +fun prefix_lines "" txt = txt
    1.18 +  | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
    1.19  
    1.20 -(*hooks for output channels: normal, warning, error*)
    1.21 -val writeln_fn = ref (std_output o suffix "\n");
    1.22 +val writeln_default = std_output o suffix "\n";
    1.23 +
    1.24 +(*hooks for various output channels*)
    1.25 +val writeln_fn = ref writeln_default;
    1.26  val priority_fn = ref (fn s => ! writeln_fn s);
    1.27  val tracing_fn = ref (fn s => ! writeln_fn s);
    1.28  val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");