WARNING_outstream
Feedback.WARNING_outstream : TextIO.outstream ref
Controlling output stream used when printing HOL_WARNING
The value of reference cell WARNING_outstream controls where
HOL_WARNING prints its argument.
The default value of WARNING_outstream is a function that prints its argument to TextIO.stdOut.
Example
> val outputs = ref ([] : string list);
val outputs = ref []: string list ref
> WARNING_outstream := (fn s => outputs := !outputs @ [s]);
val it = (): unit
> HOL_WARNING "Module" "Function" "Sufferin' Succotash!";
val it = (): unit
> outputs;
val it = ref ["<<HOL warning: Module.Function: Sufferin' Succotash!>>\n"]:
string list ref
See also
Feedback,
Feedback.HOL_WARNING,
Feedback.ERR_outstream,
Feedback.MESG_outstream,
Feedback.emit_WARNING