MESG_outstream

Feedback.MESG_outstream : TextIO.outstream ref

Reference to output stream used when printing HOL_MESG.

The value of reference cell MESG_outstream controls where HOL_MESG prints its argument.

The default value of MESG_outstream is a function that prints its argument to TextIO.stdOut.

Example

> val outputs = ref ([] : string list);
val outputs = ref []: string list ref

> MESG_outstream := (fn s => outputs := !outputs @ [s]);
val it = (): unit

> HOL_MESG "Nattering nabobs of negativity.";
val it = (): unit

> outputs;
val it = ref ["<<HOL message: Nattering nabobs of negativity.>>\n"]:
   string list ref

See also

Feedback, Feedback.HOL_MESG, Feedback.ERR_outstream, Feedback.WARNING_outstream, Feedback.emit_MESG