diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-06 21:35:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-06 22:26:57 +0100 |
| commit | cdfb6705e0a2d01b7c01d83bfe898a64ee148c34 (patch) | |
| tree | 438c12a04e313dbebbbee0f7c838f043d1a0c550 /printing/richprinter.mli | |
| parent | 1fe296cd7de29c37a735c4bef4979310c25bffb3 (diff) | |
More efficient Richpp.
We build the rich XML at once without generating the printed string.
Diffstat (limited to 'printing/richprinter.mli')
| -rw-r--r-- | printing/richprinter.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/printing/richprinter.mli b/printing/richprinter.mli index c67d52c08..41c313514 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -20,12 +20,10 @@ (** A rich pretty-print is composed of: *) type rich_pp = - (** - a raw pretty-print ; *) - string (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |