diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 21:54:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 21:54:05 +0200 |
| commit | 376b54ff8753496a54fb120e35cd1b8babb44ac9 (patch) | |
| tree | b55be0ecb60aae1a413fd7b275ccf8e32a76f1ca /lib/pp.ml | |
| parent | d873f82c5024a496e8f1a14a9839e7f377d5f4bb (diff) | |
| parent | e1f25889f88e078dac0f3b454eb16a470dd5f9ae (diff) | |
Merge PR #224 into v8.6
Diffstat (limited to 'lib/pp.ml')
| -rw-r--r-- | lib/pp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -344,8 +344,8 @@ let pp_with ?pp_tag ft strm = pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) (* pretty printing functions WITH FLUSH *) -let msg_with ft strm = - pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) +let msg_with ?pp_tag ft strm = + pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch @@ -353,7 +353,7 @@ let msg_with ft strm = (** Output to a string formatter *) let string_of_ppcmds c = - Format.fprintf Format.str_formatter "@[%a@]" msg_with c; + Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c; Format.flush_str_formatter () (* Copy paste from Util *) |