diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-05 17:56:22 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:39 +0100 |
| commit | 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (patch) | |
| tree | cf3856edc9b24a75d30f465e6e29a42962329a4a /ide | |
| parent | a8ec2dc5c330ded1ba400ef202c57e68d2533312 (diff) | |
[pp] Move terminal-specific tagging to the toplevel.
Previously, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.
This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/richpp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/richpp.mli b/ide/richpp.mli index 0fe4315b7..ea4b189ba 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -19,7 +19,7 @@ type 'annotation located = { (* XXX: The width parameter should be moved to a `formatter_property` record shared with Topfmt *) -(** [rich_pp width get_annotations ppcmds] returns the interpretation +(** [rich_pp width ppcmds] returns the interpretation of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired |