removed prs / prs_fn (broken, because it did not include \n in its
semantics, forcing writeln to add one uncoditionally);
replaced prs_fn by writeln fn;
--- a/src/Pure/library.ML Wed Nov 25 14:07:22 1998 +0100
+++ b/src/Pure/library.ML Wed Nov 25 14:11:24 1998 +0100
@@ -209,10 +209,9 @@
(*I/O and diagnostics*)
val cd: string -> unit
val pwd: unit -> string
- val prs_fn: (string -> unit) ref
+ val writeln_fn: (string -> unit) ref
val warning_fn: (string -> unit) ref
val error_fn: (string -> unit) ref
- val prs: string -> unit
val writeln: string -> unit
val warning: string -> unit
exception ERROR
@@ -1049,13 +1048,11 @@
txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
(*hooks for output channels: normal, warning, error*)
-val prs_fn = ref std_output;
+val writeln_fn = ref (std_output o suffix "\n");
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
-fun prs s = ! prs_fn s;
-fun writeln s = prs (s ^ "\n");
-
+fun writeln s = ! writeln_fn s;
fun warning s = ! warning_fn s;
(*print error message and abort to top level*)