diff options
| author | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /lib/pp.mli | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 5dd2686d14..3b1123a9dc 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -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 |