1\DOC WARNING_outstream 2 3\TYPE {WARNING_outstream : TextIO.outstream ref} 4 5\SYNOPSIS 6Controlling output stream used when printing {HOL_WARNING} 7 8\KEYWORDS 9I/O, messages, output 10 11\DESCRIBE 12The value of reference cell {WARNING_outstream} controls where {HOL_WARNING} 13prints its argument. 14 15The default value of {WARNING_outstream} is {TextIO.stdOut}. 16 17\EXAMPLE 18{ 19- val ostrm = TextIO.openOut "foo"; 20> val ostrm = <outstream> : outstream 21 22- WARNING_outstream := ostrm; 23> val it = () : unit 24 25- HOL_WARNING "Module" "Function" "Sufferin' Succotash!"; 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 warning: Module.Function: Sufferin' Succotash!>> 36} 37 38 39\SEEALSO 40Feedback, Feedback.HOL_WARNING, Feedback.ERR_outstream, Feedback.MESG_outstream, Feedback.emit_WARNING. 41\ENDDOC 42