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