changeset 3365 | 86c0d1988622 |
parent 3246 | 7f783705c7a4 |
child 3393 | e31ac367387e |
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;