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`. --- lib/pp.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 53c1fb4c3..7b21f9bbd 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -288,4 +288,3 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v let surround p = hov 1 (str"(" ++ p ++ str")") - -- cgit v1.2.3