try_user_printer : formatter -> term -> unit

SYNOPSIS
Try user-defined printers on a term.

DESCRIPTION
HOL Light allows arbitrary user printers to be inserted into the toplevel printer so that they are invoked on all applicable subterms (see install_user_printer). The call try_user_printer fmt tm attempts all installed user printers on the term tm in an implementation-defined order, sending output to the formatter fmt. If one succeeds, the call returns (), and otherwise it fails.

FAILURE CONDITIONS
Fails if no user printer is applicable to the given term (e.g. if no user printers have been installed).

EXAMPLE
After installing the printer for variables with types in the example for install_user_printer, you can try:
  # try_user_printer std_formatter `x:num`;;
  (x:num)val it : unit = ()

  # try_user_printer std_formatter `1`;;
  Exception: Failure "tryfind".

SEE ALSO
delete_user_printer, install_user_printer.