diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /lib/pp.mli | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'lib/pp.mli')
-rw-r--r-- | lib/pp.mli | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -12,6 +12,8 @@ val make_pp_emacs:unit -> unit val make_pp_nonemacs:unit -> unit +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + (** Pretty-printers. *) type std_ppcmds @@ -46,9 +48,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool (** Test emptyness. *) -val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds -(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *) - (** {6 Derived commands} *) val spc : unit -> std_ppcmds |