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