diff options
Diffstat (limited to 'printing/ppstyle.mli')
| -rw-r--r-- | printing/ppstyle.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli index e6e664f79b..b6aa0e694c 100644 --- a/printing/ppstyle.mli +++ b/printing/ppstyle.mli @@ -53,6 +53,11 @@ val init_color_output : unit -> unit with additional syle information provided by this module. Be careful this is not compatible with the Emacs mode! *) +val pp_tag : Pp.tag_handler +(** Returns the name of a style tag that is understandable by the formatters + that have been inititialized through {!init_color_output}. To be used with + {!Pp.pp_with}. *) + (** {5 Tags} *) val error_tag : t |