From 7f40ab12d4ff5ecceccbeb72555e7c4421bd9dd0 Mon Sep 17 00:00:00 2001
From: Regis-Gianas
Date: Thu, 30 Oct 2014 18:09:09 +0100
Subject: lib/Pp.ppcmd_token:         Extend this type with Ppcmd_open_tag and
 Ppcmd_close_tag. lib/Pp.ppcmd_pp_dirs:         Handle these tags with a
 straightforward translation to         corresponding Format commands.

---
 lib/pp.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index f595024e0e..4ef7b00be6 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -95,6 +95,8 @@ type 'a ppcmd_token =
   | Ppcmd_close_box
   | Ppcmd_close_tbox
   | Ppcmd_comment of int
+  | Ppcmd_open_tag of string
+  | Ppcmd_close_tag
 
 type 'a ppdir_token =
   | Ppdir_ppcmds of 'a ppcmd_token Glue.t
@@ -283,6 +285,10 @@ let pp_dirs ft =
 (*        Format.pp_open_hvbox ft 0;*)
         List.iter (pr_com ft) coms(*;
         Format.pp_close_box ft ()*)
+    | Ppcmd_open_tag name ->
+      Format.pp_open_tag ft name
+    | Ppcmd_close_tag ->
+      Format.pp_close_tag ft ()
   in
   let pp_dir = function
     | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
-- 
cgit v1.2.3