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 /printing/ppconstr.ml | |
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 'printing/ppconstr.ml')
-rw-r--r-- | printing/ppconstr.ml | 32 |
1 files changed, 7 insertions, 25 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c772f7be1..d92d83275 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -23,32 +23,14 @@ open Misctypes module Tag = struct - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["constr"; "keyword"] + let keyword = "constr.keyword" + let evar = "constr.evar" + let univ = "constr.type" + let notation = "constr.notation" + let variable = "constr.variable" + let reference = "constr.reference" + let path = "constr.path" - let evar = - let style = Terminal.make ~fg_color:`LIGHT_BLUE () in - Ppstyle.make ~style ["constr"; "evar"] - - let univ = - let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in - Ppstyle.make ~style ["constr"; "type"] - - let notation = - let style = Terminal.make ~fg_color:`WHITE () in - Ppstyle.make ~style ["constr"; "notation"] - - let variable = - Ppstyle.make ["constr"; "variable"] - - let reference = - let style = Terminal.make ~fg_color:`LIGHT_GREEN () in - Ppstyle.make ~style ["constr"; "reference"] - - let path = - let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in - Ppstyle.make ~style ["constr"; "path"] end let do_not_tag _ x = x |