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`.
---
 plugins/ltac/pptactic.ml | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d9410a0885..dc418d530e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -29,17 +29,10 @@ open Printer
 
 module Tag =
 struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["tactic"; "keyword"]
 
-  let primitive =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["tactic"; "primitive"]
-
-  let string =
-    let style = Terminal.make ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["tactic"; "string"]
+  let keyword   = "tactic.keyword"
+  let primitive = "tactic.primitive"
+  let string    = "tactic.string"
 
 end
 
-- 
cgit v1.2.3