From 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Dec 2016 17:56:22 +0100
Subject: [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`.
---
 ide/richpp.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/richpp.mli b/ide/richpp.mli
index 0fe4315b7a..ea4b189ba8 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
-- 
cgit v1.2.3