aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-15 18:21:14 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-15 18:28:33 +0100
commitf3e126bc3e8b12bb9e9d2cd62b9de0dd818c85ef (patch)
treedfaaa65d0162f807d4c2fdf0d05aac2ad29a9427 /printing
parent74234f18661a7ece3f5d141196a75784e3c7f6da (diff)
Setting a keyword tag in Ppconstr.
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml12
1 files changed, 9 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1481ea191..78ba40114 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -803,11 +803,17 @@ end) = struct
end
-(** Preserve the initial behaviour of Ppconstr by instantiating Make
- with tagging functions that do nothing. *)
+module Tag =
+struct
+ let keyword = Ppstyle.make ["constr"; "keyword"]
+end
+
+(** Instantiating Make with tagging functions that only add style
+ information. *)
include Make (struct
let do_not_tag _ x = x
- let tag_keyword = do_not_tag ()
+ let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+ let tag_keyword = tag Tag.keyword
let tag_unparsing = do_not_tag
let tag_constr_expr = do_not_tag
end)