From fb0caf14daff2e433dfc33ca564d49b26f7e8fb4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 18 May 2020 22:12:29 +0200
Subject: [topfmt] Set formatter + flush fix

Closes #12351.

We set the parameters of the redirect formatter to be same than the
ones in stdout.

I guess the original semantics was to ignore the parameters, so I'm
unsure we want to do this.

While we are a it, we include a fix on the formatter, which _must_ be
flushed before closing its associated channel.
---
 vernac/topfmt.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'vernac')

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 2d8734ff7f..a28d8f605b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -404,6 +404,7 @@ let with_output_to_file fname func input =
   let channel = open_out (String.concat "." [fname; "out"]) in
   let old_fmt = !std_ft, !err_ft, !deep_ft in
   let new_ft = Format.formatter_of_out_channel channel in
+  set_gp new_ft (get_gp !std_ft);
   std_ft := new_ft;
   err_ft := new_ft;
   deep_ft := new_ft;
@@ -412,6 +413,7 @@ let with_output_to_file fname func input =
     std_ft := Util.pi1 old_fmt;
     err_ft := Util.pi2 old_fmt;
     deep_ft := Util.pi3 old_fmt;
+    Format.pp_print_flush new_ft ();
     close_out channel;
     output
   with reraise ->
@@ -419,6 +421,7 @@ let with_output_to_file fname func input =
     std_ft := Util.pi1 old_fmt;
     err_ft := Util.pi2 old_fmt;
     deep_ft := Util.pi3 old_fmt;
+    Format.pp_print_flush new_ft ();
     close_out channel;
     Exninfo.iraise reraise
 
-- 
cgit v1.2.3