diff options
| author | Pierre-Marie Pédrot | 2014-11-17 10:43:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-17 10:49:34 +0100 |
| commit | 462b733b2df486dbf123638418159ef8c4ee93a2 (patch) | |
| tree | a86259633c048fb6543349eb311cefff753deb59 /printing/ppstyle.mli | |
| parent | 659ca3902a144259ec449473e95df1b3eda1b6de (diff) | |
Default styles for printing tags.
They should be rather sensible, but de gustibus & coloribus...
Diffstat (limited to 'printing/ppstyle.mli')
| -rw-r--r-- | printing/ppstyle.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli index 700ec4314e..e6e664f79b 100644 --- a/printing/ppstyle.mli +++ b/printing/ppstyle.mli @@ -14,8 +14,9 @@ type t (** Style tags *) -val make : string list -> t -(** Create a new tag with the given name. Each name must be unique. *) +val make : ?style:Terminal.style -> string list -> t +(** Create a new tag with the given name. Each name must be unique. The optional + style is taken as the default one. *) val repr : t -> string list (** Gives back the original name of the style tag where each string has been |