1\DOC ERR_outstream
2
3\TYPE {ERR_outstream : TextIO.outstream ref}
4
5\SYNOPSIS
6Reference to output stream used when printing {HOL_ERR}
7
8\KEYWORDS
9I/O, error, exceptions, output
10
11\DESCRIBE
12The value of reference cell {ERR_outstream} controls where {Raise}
13prints its argument.
14
15The default value of {ERR_outstream} is {TextIO.stdErr}.
16
17\EXAMPLE
18{
19- val ostrm = TextIO.openOut "foo";
20> val ostrm = <outstream> : outstream
21
22- ERR_outstream := ostrm;
23> val it = () : unit
24
25- Raise (mk_HOL_ERR "Foo" "bar" "incomprehensible input");
26! Uncaught exception:
27! HOL_ERR
28
29- TextIO.closeOut ostrm;
30> val it = () : unit
31
32- val istrm = TextIO.openIn "foo";
33> val istrm = <instream> : instream
34
35- print (TextIO.inputAll istrm);
36
37Exception raised at Foo.bar:
38incomprehensible input
39}
40
41
42\SEEALSO
43Feedback, Feedback.HOL_ERR, Feedback.Raise, Feedback.MESG_outstream, Feedback.WARNING_outstream.
44\ENDDOC
45