diff options
| author | Regis-Gianas | 2014-10-30 20:15:47 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | d21183a81fb73cd20ace5213cfe46c82250db38b (patch) | |
| tree | 7bc9513b6d0ae48dc4faa982357b40a2b4e878b8 | |
| parent | 00bb36da0696b1442bf4e0bb1a657e3de8c92b1e (diff) | |
lib/Pp: Publish combinators for tags opening and closing.
| -rw-r--r-- | lib/pp.ml | 4 | ||||
| -rw-r--r-- | lib/pp.mli | 11 |
2 files changed, 12 insertions, 3 deletions
@@ -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 *) diff --git a/lib/pp.mli b/lib/pp.mli index 539ef0f410..dad4ed6abb 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -77,6 +77,11 @@ val tb : unit -> std_ppcmds val close : unit -> std_ppcmds val tclose : unit -> std_ppcmds +(** {6 Opening and closing of tags} *) + +val open_tag : string -> std_ppcmds +val close_tag : unit -> std_ppcmds + (** {6 Sending messages to the user} *) type message_level = Feedback.message_level = | Debug of string @@ -100,11 +105,11 @@ val msg_notice : std_ppcmds -> unit (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) val msg_warning : std_ppcmds -> unit -(** Message indicating that something went wrong, but without serious +(** Message indicating that something went wrong, but without serious consequences. *) val msg_error : std_ppcmds -> unit -(** Message indicating that something went really wrong, though still +(** Message indicating that something went really wrong, though still recoverable; otherwise an exception would have been raised. *) val msg_debug : std_ppcmds -> unit @@ -171,7 +176,7 @@ val pr_nth : int -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds (** Concatenation of the list contents, without any separator. - Unlike all other functions below, [prlist] works lazily. If a strict + Unlike all other functions below, [prlist] works lazily. If a strict behavior is needed, use [prlist_strict] instead. *) val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds |