src/Pure/library.ML
changeset 5966 60f80b2a2777
parent 5949 1e1d997e5c10
child 6282 589671bebbb3
--- 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*)