flushOut ensures that no recent error message are lost (not certain this is
authorpaulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 336586c0d1988622
parent 3364 8f225296fade
child 3366 2402c6ab1561
flushOut ensures that no recent error message are lost (not certain this is
necessary)
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue May 27 17:49:52 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Fri May 30 15:14:59 1997 +0200
     1.3 @@ -747,7 +747,9 @@
     1.4  		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
     1.5  
     1.6  exception ERROR;
     1.7 -fun error msg = (!error_fn msg; raise ERROR);
     1.8 +fun error msg = (!error_fn msg;
     1.9 +		 TextIO.flushOut TextIO.stdOut; 
    1.10 +		 raise ERROR);
    1.11  fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
    1.12  
    1.13  fun assert p msg = if p then () else error msg;