ERR_to_string

Feedback.ERR_to_string : (error_record -> string) ref

Alterable function for formatting HOL_ERR.

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"];
val alt_ERR_report = fn:
   {message: string, origin_function: string, origin_structure: string} ->
     string

> ERR_to_string := alt_ERR_report;
Exception- Type error in function application.
   Function: := :
      (hol_error -> string) ref * (hol_error -> string) -> unit
   Argument: (ERR_to_string, alt_ERR_report) :
      (hol_error -> string) ref *
      ({message: string,
        origin_function: string, origin_structure: string} -> string)
   Reason:
      Can't unify hol_error to
         {message: string,
           origin_function: string, origin_structure: string}
         (Incompatible types)
Fail "Static Errors" raised

> Raise (HOL_ERR {origin_structure = "Foo",
                origin_function = "bar",
                message = "incomprehensible input"});
Exception- Type error in function application.
   Function: HOL_ERR : hol_error -> exn
   Argument:
      {origin_structure = "Foo", origin_function = "bar",
        message = "incomprehensible input"} :
      {message: string,
        origin_function: string, origin_structure: string}
   Reason:
      Can't unify hol_error to
         {message: string,
           origin_function: string, origin_structure: string}
         (Incompatible types)
Fail "Static Errors" raised

See also

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