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