1\DOC MESG_outstream 2 3\TYPE {MESG_outstream : TextIO.outstream ref} 4 5\SYNOPSIS 6Reference to output stream used when printing {HOL_MESG}. 7 8\KEYWORDS 9I/O, messages, output 10 11\DESCRIBE 12The value of reference cell {MESG_outstream} controls where {HOL_MESG} 13prints its argument. 14 15The default value of {MESG_outstream} is {TextIO.stdOut}. 16 17\EXAMPLE 18{ 19- val ostrm = TextIO.openOut "foo"; 20> val ostrm = <outstream> : outstream 21 22- MESG_outstream := ostrm; 23> val it = () : unit 24 25- HOL_MESG "Nattering nabobs of negativity."; 26> val it = () : unit 27 28- TextIO.closeOut ostrm; 29> val it = () : unit 30 31- val istrm = TextIO.openIn "foo"; 32> val istrm = <instream> : instream 33 34- print (TextIO.inputAll istrm); 35<<HOL message: Nattering nabobs of negativity.>> 36} 37 38 39\SEEALSO 40Feedback, Feedback.HOL_MESG, Feedback.ERR_outstream, Feedback.WARNING_outstream, Feedback.emit_MESG. 41\ENDDOC 42