----------------------------------------------------------------------
ERR_to_string                                               (Feedback)
----------------------------------------------------------------------
ERR_to_string : (error_record -> string) ref

SYNOPSIS
Alterable function for formatting {HOL_ERR}.

KEYWORDS
exception, error, formatting

DESCRIBE
{ERR_to_string} is a reference to a function for formatting the argument
to an application of {HOL_ERR}. It can be used to customize {Raise}.

The default value of {ERR_to_string} is {format_ERR}.

EXAMPLE

- fun alt_ERR_report {origin_structure,origin_function,message} =
     String.concat["This just in from ",origin_function, " at ",
                   origin_structure, " : ", message, "\n"];

- ERR_to_string := alt_ERR_report;

- Raise (HOL_ERR {origin_structure = "Foo",
                  origin_function = "bar",
                  message = "incomprehensible input"});

This just in from bar at Foo : incomprehensible input
! Uncaught exception:
! HOL_ERR




SEEALSO
Feedback, Feedback.error_record, Feedback.HOL_ERR, Feedback.Raise,
Feedback.MESG_to_string, Feedback.WARNING_to_string.

----------------------------------------------------------------------