diff options
| author | Pierre-Marie Pédrot | 2015-08-15 19:27:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-15 20:05:40 +0200 |
| commit | 54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1 (patch) | |
| tree | 5b9f6879291476b13c81ae172b22836fe4c72f0c /lib/richpp.mli | |
| parent | 98618cfb6b326b70da29348bc5d212e41086f473 (diff) | |
More invariants in Richpp.
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
Diffstat (limited to 'lib/richpp.mli')
| -rw-r--r-- | lib/richpp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/richpp.mli b/lib/richpp.mli index 5eb0e7b3b0..3f6463c88a 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -23,7 +23,7 @@ type 'annotation located = { annotation. If this function returns [None], then no annotation is put. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - (string, 'annotation located) Xml_datatype.gxml + (unit, 'annotation located) Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -37,5 +37,5 @@ val annotations_positions : val xml_of_rich_pp : ('annotation -> string) -> ('annotation -> (string * string) list) -> - (string, 'annotation located) Xml_datatype.gxml -> + ('a, 'annotation located) Xml_datatype.gxml -> Xml_datatype.xml |