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.

1 files changed, 6 insertions, 0 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index f595024e0..4ef7b00be 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