src/Pure/library.ML
changeset 1580 e3fd931e6095
parent 1576 af8f43f742a0
child 1592 d89d5ff2397f
     1.1 --- a/src/Pure/library.ML	Thu Mar 14 16:40:18 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Mar 15 12:01:19 1996 +0100
     1.3 @@ -703,14 +703,22 @@
     1.4  
     1.5  (** input / output **)
     1.6  
     1.7 -fun prs s = output (std_out, s);
     1.8 +val prs_fn = ref(fn s => output (std_out, s));
     1.9 +
    1.10 +fun prs s = !prs_fn s;
    1.11  fun writeln s = prs (s ^ "\n");
    1.12  
    1.13 +(*print warning*)
    1.14 +val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
    1.15 +fun warning s = !warning_fn ("Warning: " ^ s);
    1.16  
    1.17  (*print error message and abort to top level*)
    1.18 +
    1.19 +val error_fn = ref(fn s => output (std_out, s ^ "\n"));
    1.20 +
    1.21  exception ERROR;
    1.22 -fun error msg = (writeln msg; raise ERROR);
    1.23 -fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
    1.24 +fun error msg = (!error_fn msg; raise ERROR);
    1.25 +fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
    1.26  
    1.27  fun assert p msg = if p then () else error msg;
    1.28  fun deny p msg = if p then error msg else ();