# 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);