diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 31 | ||||
| -rw-r--r-- | lib/pp.mli | 19 |
2 files changed, 50 insertions, 0 deletions
@@ -37,6 +37,37 @@ end = struct let map = List.map end +module Tag : +sig + type t + type 'a key + val create : string -> 'a key + val inj : 'a -> 'a key -> t + val prj : t -> 'a key -> 'a option +end = +struct + (** See module {Dyn} for more details. *) + + type t = int * Obj.t + + type 'a key = int + + let dyntab = ref (Int.Map.empty : string Int.Map.t) + + let create (s : string) = + let hash = Hashtbl.hash s in + let () = assert (not (Int.Map.mem hash !dyntab)) in + let () = dyntab := Int.Map.add hash s !dyntab in + hash + + let inj x h = (h, Obj.repr x) + + let prj (nh, rv) h = + if Int.equal h nh then Some (Obj.magic rv) + else None + +end + open Pp_control (* This should not be used outside of this file. Use 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 |