aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorRegis-Gianas2014-10-30 20:15:47 +0100
committerRegis-Gianas2014-11-04 22:51:35 +0100
commitd21183a81fb73cd20ace5213cfe46c82250db38b (patch)
tree7bc9513b6d0ae48dc4faa982357b40a2b4e878b8 /lib/pp.ml
parent00bb36da0696b1442bf4e0bb1a657e3de8c92b1e (diff)
lib/Pp: Publish combinators for tags opening and closing.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 4ef7b00be6..dff0fb0adb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -199,6 +199,10 @@ let tb () = Glue.atom(Ppcmd_open_box Pp_tbox)
let close () = Glue.atom(Ppcmd_close_box)
let tclose () = Glue.atom(Ppcmd_close_tbox)
+(* Opening and closed of tags *)
+let open_tag t = Glue.atom(Ppcmd_open_tag t)
+let close_tag () = Glue.atom(Ppcmd_close_tag)
+
let eval_ppcmds l = l
(* In new syntax only double quote char is escaped by repeating it *)