# HG changeset patch
# User wenzelm
# Date 911999484 -3600
# Node ID 60f80b2a27771327f0ae13d424ccc2e9aa34e3a2
# Parent  f91212fd2c7c4cde9652bfbcb54adb47a55ace6d
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;

diff -r f91212fd2c7c -r 60f80b2a2777 src/Pure/library.ML
--- 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*)