[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.

(cherry picked from commit fb0caf1)

doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:Redirect now obeys the :opt:`Printing Width` and
+  :opt:`Printing Depth` flags.
+  (`#12358 <https://github.com/coq/coq/pull/12358>`_,
+  by Emilio Jesus Gallego Arias).

test-suite/misc/redirect_printing.out

@@ -0,0 +1,2 @@
+nat_ind
+     : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

test-suite/misc/redirect_printing.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+$coqc misc/redirect_printing.v
+diff -u redirect_test.out misc/redirect_printing.out

test-suite/misc/redirect_printing.v

@@ -0,0 +1,2 @@
+Set Printing Width 999999.
+Redirect "redirect_test" Check nat_ind.

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,13 +413,15 @@ 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 ->
     let reraise = Exninfo.capture reraise in
     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