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