ERR_outstream

Feedback.ERR_outstream : (string -> unit) ref

Reference to output stream used when printing HOL_ERR

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

The default value of ERR_outstream is a function that prints its argument to TextIO.stdErr.

Example

> val outputs = ref ([] : string list);
val outputs = ref []: string list ref

> ERR_outstream := (fn s => outputs := !outputs @ [s]);
val it = (): unit

> Raise (mk_HOL_ERR "Foo" "bar" "incomprehensible input");
Exception- The type of (it) contains a free type variable. Setting it to a unique
   monotype.
HOL_ERR (at Foo.bar: incomprehensible input) raised

> outputs;
val it = ref ["\nException raised at Foo.bar: incomprehensible input\n"]:
   string list ref

See also

Feedback, Feedback.HOL_ERR, Feedback.Raise, Feedback.MESG_outstream, Feedback.WARNING_outstream