aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-12-05 17:56:22 +0100
committerEmilio Jesus Gallego Arias2017-03-21 15:51:39 +0100
commit3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (patch)
treecf3856edc9b24a75d30f465e6e29a42962329a4a /printing
parenta8ec2dc5c330ded1ba400ef202c57e68d2533312 (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')
-rw-r--r--printing/ppconstr.ml32
-rw-r--r--printing/printmod.ml10
2 files changed, 11 insertions, 31 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c772f7be16..d92d832759 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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 521b4ec2ae..baa1b8d791 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -28,12 +28,10 @@ open Goptions
module Tag =
struct
- let definition =
- let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
- Ppstyle.make ~style ["module"; "definition"]
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["module"; "keyword"]
+
+ let definition = "module.definition"
+ let keyword = "module.keyword"
+
end
let tag t s = Pp.tag t s