diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-10-30 20:15:47 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:35 +0100 |
| commit | d21183a81fb73cd20ace5213cfe46c82250db38b (patch) | |
| tree | 7bc9513b6d0ae48dc4faa982357b40a2b4e878b8 /lib/pp.mli | |
| parent | 00bb36da0696b1442bf4e0bb1a657e3de8c92b1e (diff) | |
lib/Pp: Publish combinators for tags opening and closing.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 539ef0f41..dad4ed6ab 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 |