diff options
Diffstat (limited to 'ide/richpp.mli')
| -rw-r--r-- | ide/richpp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/richpp.mli b/ide/richpp.mli index f2ba15d22..84adc61ca 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,7 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml +val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -47,5 +47,5 @@ type richpp = Xml_datatype.xml (** Type of text with style annotations *) -val richpp_of_pp : int -> Pp.std_ppcmds -> richpp +val richpp_of_pp : int -> Pp.t -> richpp (** Extract style information from formatted text *) |