1.1 --- a/src/Pure/library.ML	Fri Nov 20 10:37:12 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Nov 21 12:16:15 1998 +0100
     1.3 @@ -129,6 +129,8 @@
     1.4    val commas_quote: string list -> string
     1.5    val cat_lines: string list -> string
     1.6    val space_explode: string -> string -> string list
     1.7 +  val std_output: string -> unit
     1.8 +  val prefix_lines: string -> string -> string
     1.9    val split_lines: string -> string list
    1.10    val suffix: string -> string -> string
    1.11    val unsuffix: string -> string -> string
    1.12 @@ -1040,26 +1042,21 @@
    1.13  val cd = OS.FileSys.chDir;
    1.14  val pwd = OS.FileSys.getDir;
    1.15  
    1.16 +fun std_output s =
    1.17 +  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.18  
    1.19 -local
    1.20 -  fun out s =
    1.21 -    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.22 -
    1.23 -  fun prefix_lines prfx txt =
    1.24 -    txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
    1.25 -in
    1.26 +fun prefix_lines prfx txt =
    1.27 +  txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
    1.28  
    1.29  (*hooks for output channels: normal, warning, error*)
    1.30 -val prs_fn = ref (fn s => out s);
    1.31 -val warning_fn = ref (fn s => out (prefix_lines "### " s));
    1.32 -val error_fn = ref (fn s => out (prefix_lines "*** " s));
    1.33 -
    1.34 -end;
    1.35 +val prs_fn = ref (fn s => std_output s);
    1.36 +val warning_fn = ref (fn s => std_output (prefix_lines "### " s));
    1.37 +val error_fn = ref (fn s => std_output (prefix_lines "*** " s));
    1.38  
    1.39  fun prs s = !prs_fn s;
    1.40  fun writeln s = prs (s ^ "\n");
    1.41  
    1.42 -fun warning s = !warning_fn s;
    1.43 +fun warning s = ! warning_fn s;
    1.44  
    1.45  (*print error message and abort to top level*)
    1.46  exception ERROR;