# HG changeset patch
# User wenzelm
# Date 911905155 -3600
# Node ID 1e1d997e5c10bffb70d7c448f68ab39117327aad
# Parent  f389885afb929721a7f8b2ab1f72d3a66a8d3696
fixed prefix_lines: *separate* by \n;

diff -r f389885afb92 -r 1e1d997e5c10 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 24 11:58:38 1998 +0100
+++ b/src/Pure/library.ML	Tue Nov 24 11:59:15 1998 +0100
@@ -1046,21 +1046,21 @@
   (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
 
 fun prefix_lines prfx txt =
-  txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
+  txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
 
 (*hooks for output channels: normal, warning, error*)
-val prs_fn = ref (fn s => std_output s);
-val warning_fn = ref (fn s => std_output (prefix_lines "### " s));
-val error_fn = ref (fn s => std_output (prefix_lines "*** " s));
+val prs_fn = ref std_output;
+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 prs s = ! prs_fn s;
 fun writeln s = prs (s ^ "\n");
 
 fun warning s = ! warning_fn s;
 
 (*print error message and abort to top level*)
 exception ERROR;
-fun error_msg s = !error_fn s;
+fun error_msg s = ! error_fn s;
 fun error s = (error_msg s; raise ERROR);
 fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);