try_user_color_printer : formatter -> term -> unit
- SYNOPSIS
-
Try user-defined color 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 and install_user_color_printer).
The call try_user_color_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).
- SEE ALSO
-
delete_user_color_printer, delete_user_printer, install_user_color_printer,
install_user_printer, try_user_printer.