Feedback.ERR_outstream

STRUCTURE

SYNOPSIS

Reference to output stream used when printing HOL_ERR

DESCRIPTION

The value of reference cell ERR_outstream controls where Raise prints its argument.

The default value of ERR_outstream is TextIO.stdErr.

EXAMPLE

- val ostrm = TextIO.openOut "foo";
> val ostrm = <outstream> : outstream

- ERR_outstream := ostrm;
> val it = () : unit

- Raise (mk_HOL_ERR "Foo" "bar" "incomprehensible input");
! Uncaught exception:
! HOL_ERR

- TextIO.closeOut ostrm;
> val it = () : unit

- val istrm = TextIO.openIn "foo";
> val istrm = <instream> : instream

- print (TextIO.inputAll istrm);

Exception raised at Foo.bar:
incomprehensible input

SEEALSO

Feedback, HOL_ERR, Raise, MESG_outstream, WARNING_outstream