Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.

2 files changed, 23 insertions, 0 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 9667f7270e..30bc30a9ad 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -448,6 +448,27 @@ let logger = ref std_logger
 let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
 let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
 
+let ft_logger old_logger ft ~id level mesg = match level with
+  | Debug _ -> msgnl_with ft (debugbody mesg)
+  | Info -> msgnl_with ft (infobody mesg)
+  | Notice -> msgnl_with ft mesg
+  | Warning -> old_logger ~id:id level mesg
+  | Error -> old_logger ~id:id level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
 
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
diff --git a/lib/pp.mli b/lib/pp.mli
index e20e5ca82a..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