diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index f29f9b2f3..d5983c4a2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -82,6 +82,25 @@ val tclose : unit -> std_ppcmds (** {6 Opening and closing of tags} *) +module Tag : +sig + type t + (** Type of tags. Tags are dynamic types comparable to {Dyn.t}. *) + + type 'a key + (** Keys used to inject tags *) + + val create : string -> 'a key + (** Create a key with the given name. Two keys cannot share the same name, if + ever this is the case this function raises an assertion failure. *) + + val inj : 'a -> 'a key -> t + (** Inject an object into a tag. *) + + val prj : t -> 'a key -> 'a option + (** Project an object from a tag. *) +end + val tag : string -> std_ppcmds -> std_ppcmds val open_tag : string -> std_ppcmds val close_tag : unit -> std_ppcmds |